Merge remote-tracking branch 'origin/master' into stm+doc_hook

1 files changed, 6 insertions, 13 deletions

diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 20a2db7ca2..69e2a209eb 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -230,12 +230,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   in
   (* XXX: Capturing sigma here... bad bad *)
   let hook = Lemmas.mk_hook (hook sigma) in
-  (* XXX: Grounding non-ground terms here... bad bad *)
-  let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in
-  let fullctyp = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in
   Obligations.check_evars env sigma;
   let evars, _, evars_def, evars_typ =
-    Obligations.eterm_obligations env recname sigma 0 fullcoqc fullctyp
+    Obligations.eterm_obligations env recname sigma 0 def typ
   in
   let ctx = Evd.evar_universe_context sigma in
     ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl
@@ -246,7 +243,7 @@ let out_def = function
   | None -> user_err Pp.(str "Program Fixpoint needs defined bodies.")
 
 let collect_evars_of_term evd c ty =
-  let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in
+  let evars = Evar.Set.union (Evd.evars_of_term evd c) (Evd.evars_of_term evd ty) in
   Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
   evars (Evd.from_ctx (Evd.evar_universe_context evd))
 
@@ -262,17 +259,13 @@ let do_program_recursive local poly fixkind fixl ntns =
   let evd = nf_evar_map_undefined evd in
   let collect_evars id def typ imps =
     (* Generalize by the recursive prototypes  *)
-    let def =
-      EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign)
-    and typ =
-      (* Worrying... *)
-      EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign)
-    in
+    let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in
+    let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in
     let evm = collect_evars_of_term evd def typ in
     let evars, _, def, typ =
       Obligations.eterm_obligations env id evm
-        (List.length rec_sign) def typ
-    in (id, def, typ, imps, evars)
+        (List.length rec_sign) def typ in
+    (id, def, typ, imps, evars)
   in
   let (fixnames,fixrs,fixdefs,fixtypes) = fix in
   let fiximps = List.map pi2 info in