diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-29 08:27:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-29 08:27:03 +0000 |
| commit | 7e2f953c3c19904616c43990fada92e762aadec9 (patch) | |
| tree | 8268d6e2b66ccdcce69df129ed98703e87f141b0 /toplevel | |
| parent | ee711f8994d5e2e94cc61292ac6aab125c23df1c (diff) | |
Made tclABSTRACT normalize evars before saying it does not support
them. This was the cause of the failure of compilation of
CyclicAxioms after "replace" starting supporting open constrs (r13206).
Seized the opportunity to clean a little bit things around nf_evar,
whd_evar, check_evars, etc.
Removed obsolete printer mod_self_id from dev/db.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13214 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/classes.ml | 6 | ||||
| -rw-r--r-- | toplevel/command.ml | 6 | ||||
| -rw-r--r-- | toplevel/lemmas.ml | 2 |
3 files changed, 7 insertions, 7 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index d16147024..62a7ebb44 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -184,7 +184,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props let _, ty_constr = instance_constructor k (List.rev subst) in let termtype = let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - Evarutil.nf_isevar !evars t + Evarutil.nf_evar !evars t in Evarutil.check_evars env Evd.empty !evars termtype; let cst = Declare.declare_internal_constant id @@ -249,8 +249,8 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props let term = Termops.it_mkLambda_or_LetIn def ctx in term, termtype in - let termtype = Evarutil.nf_isevar !evars termtype in - let term = Evarutil.nf_isevar !evars term in + let termtype = Evarutil.nf_evar !evars termtype in + let term = Evarutil.nf_evar !evars term in let evm = undefined_evars !evars in Evarutil.check_evars env Evd.empty !evars termtype; if Evd.is_empty evm then diff --git a/toplevel/command.ml b/toplevel/command.ml index 8d840a458..4259ccb81 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -73,7 +73,7 @@ let interp_definition boxed bl red_option c ctypopt = match ctypopt with None -> let c, imps2 = interp_constr_evars_impls ~evdref ~fail_evar:false env_bl c in - let body = nf_isevar !evdref (it_mkLambda_or_LetIn c ctx) in + let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in check_evars env Evd.empty !evdref body; imps1@imps2, { const_entry_body = body; @@ -83,8 +83,8 @@ let interp_definition boxed bl red_option c ctypopt = | Some ctyp -> let ty, impls = interp_type_evars_impls ~evdref ~fail_evar:false env_bl ctyp in let c, imps2 = interp_casted_constr_evars_impls ~evdref ~fail_evar:false env_bl c ty in - let body = nf_isevar !evdref (it_mkLambda_or_LetIn c ctx) in - let typ = nf_isevar !evdref (it_mkProd_or_LetIn ty ctx) in + let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in + let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in check_evars env Evd.empty !evdref body; check_evars env Evd.empty !evdref typ; imps1@imps2, diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 01cfd22e8..efb0595ab 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -320,7 +320,7 @@ let start_proof_com kind thms hook = Sign.iter_rel_context (check_evars env Evd.empty !evdref) ctx; let ids = List.map pi1 ctx in (compute_proof_name (fst kind) sopt, - (nf_isevar !evdref (it_mkProd_or_LetIn t' ctx), + (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), (ids, imps @ lift_implicits (List.length ids) imps'), guard))) thms in |