Merge pull request #876 from Tragicus/collect_goals

Fold with binders in collect-goals

Author: gares

elpi/elpi-ltac.elpi

@@ -87,10 +87,10 @@ open T (nabla G) O :- (pi x\ open T (G x) (NG x)), private.distribute-nabla NG O
 open _ (seal (goal _ _ _ Solution _)) [] :- not (var Solution), !. % solved by side effect
 open T (seal (goal Ctx _ _ _ _ as G)) O :-
   std.filter Ctx private.not-already-assumed Ctx1,
-  (Ctx1 => T G O),
-  if (var O)
-     (G = goal _ _ _ P _, coq.ltac.collect-goals P O1 O2, std.append O1 O2 O)
-     true.
+  Ctx1 => (T G O,
+    if (var O)
+       (G = goal _ _ _ P _, coq.ltac.collect-goals P O1 O2, std.append O1 O2 O)
+       true).
 
 % helper code ---------------------------------------------------------------
 
@@ -127,4 +127,4 @@ func not-already-assumed prop.
 not-already-assumed (decl X _ _Ty) :- not(decl X _ _ ; def X _ _ _).
 not-already-assumed (def X _ _Ty _Bo) :- not(decl X _ _ ; def X _ _ _).
 
-}}
+}}

src/rocq_elpi_builtins.ml

@@ -3896,24 +3896,24 @@ fold_left over the terms, letin body comes before the type).
     (fun proof _ shelved ~depth proof_context constraints state ->
       let env = proof_context.env in
       let sigma = get_sigma state in
-      let evars_of_term evd c =
-        let rec evrec (acc_set,acc_rev_l as acc) c =
-          let c = EConstr.whd_evar evd c in
+      let evars_of_term c =
+        let rec evrec env (acc_set,acc_rev_l as acc) c =
           match EConstr.kind sigma c with
           | Constr.Evar (n, l) ->
-            if Evar.Set.mem n acc_set then acc
+            if Evar.Set.mem n acc_set then
+              acc
             else
               let acc = Evar.Set.add n acc_set, n :: acc_rev_l in
-              SList.Skip.fold evrec acc l
+              SList.Skip.fold (evrec env) acc l
           | Constr.Proj (_, _, c) ->
             let t = Retyping.get_type_of env sigma c in
-            let acc = evrec acc t in
-            evrec acc c
-          | _ -> EConstr.fold sigma evrec acc c
+            let acc = evrec env acc t in
+            evrec env acc c
+          | _ -> Termops.fold_constr_with_full_binders env sigma EConstr.push_rel evrec env acc c
         in
-        let _, rev_l = evrec (Evar.Set.empty, []) c in
+        let _, rev_l = evrec env (Evar.Set.empty, []) c in
         List.rev rev_l in
-      let subgoals = evars_of_term sigma proof in
+      let subgoals = evars_of_term proof in
       let free_evars =
         let cache = Evarutil.create_undefined_evars_cache () in
         let map ev =