diff options
| author | Hugo Herbelin | 2018-11-01 23:26:06 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-13 18:23:58 +0200 |
| commit | 6211fd6e067e781a160db8765dd87067428048f2 (patch) | |
| tree | fa36209357839891624f3c3a88a042e45485e41e /vernac/comProgramFixpoint.ml | |
| parent | 9f11eeefc204bdad029b66f30bc6c52377af63ae (diff) | |
Moving Evd.evars_of_term from constr to econstr + consequences.
This impacts a lot of code, apparently in the good, removing several
conversions back and forth constr.
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 17 |
1 files changed, 5 insertions, 12 deletions
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 20a2db7ca2..3befdc5885 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 @@ -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 |