diff options
-rw-r--r-- | pretyping/evarutil.ml | 51 | ||||
-rw-r--r-- | pretyping/evarutil.mli | 2 | ||||
-rw-r--r-- | pretyping/evd.ml | 9 | ||||
-rw-r--r-- | pretyping/unification.ml | 4 |
4 files changed, 31 insertions, 35 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 759157b30..746d2cd8e 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -318,6 +318,30 @@ let real_clean env isevars ev evi args rhs = then error_not_clean env (evars_of !evd) ev body (evar_source ev !evd); (!evd,body) +(* [typed_evar_define evd sp c] (tactic style) + * + * Defines evar [sp] with term [c] in evar context [evd]. + * [c] is typed in the context of [sp] and evar context [evd] with + * [sp] removed to avoid circular definitions. + * No unification is performed in order to assert that [c] has the + * correct type. + * +let typed_evar_define sp c evd = + let sigma = evars_of evd in + let spdecl = Evd.map sigma sp in + let env = evar_env spdecl in + let _ = + (* Do not consider the metamap because evars may not depend on metas *) + try Typing.check env (Evd.rmv sigma sp) c spdecl.evar_concl + with + Not_found -> error "Instantiation contains unlegal variables" + | (Type_errors.TypeError (e, Type_errors.UnboundVar v))-> + errorlabstrm "typed_evar_define" + (str "Cannot use variable " ++ pr_id v ++ str " to define " ++ + str (string_of_existential sp)) in + Evd.evar_define sp c evd +*) + (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated * evar, i.e. tries to find the body ?sp for lhs=mkEvar (sp,args) * ?sp [ sp.hyps \ args ] unifies to rhs @@ -349,33 +373,6 @@ let evar_define env (ev,argsv) rhs isevars = let isevars'' = Evd.evar_define ev body isevars' in isevars'',[ev] -(* [w_Define evd sp c] (tactic style) - * - * Defines evar [sp] with term [c] in evar context [evd]. - * [c] is typed in the context of [sp] and evar context [evd] with - * [sp] removed to avoid circular definitions. - * No unification is performed in order to assert that [c] has the - * correct type. - *) -let w_Define sp c evd = - let sigma = evars_of evd in - if not (Evd.in_dom sigma sp) then - error "w_Define: cannot define undeclared evar"; - if Evd.is_defined sigma sp then - error "w_Define: cannot define evar twice"; - let spdecl = Evd.map sigma sp in - let env = evar_env spdecl in - let _ = - (* Do not consider the metamap because evars may not depend on metas *) - try Typing.check env (Evd.rmv sigma sp) c spdecl.evar_concl - with - Not_found -> error "Instantiation contains unlegal variables" - | (Type_errors.TypeError (e, Type_errors.UnboundVar v))-> - errorlabstrm "w_Define" - (str "Cannot use variable " ++ pr_id v ++ str " to define " ++ - str (string_of_existential sp)) in - let spdecl' = { spdecl with evar_body = Evar_defined c } in - evars_reset_evd (Evd.add sigma sp spdecl') evd (*-------------------*) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index e8669e5fa..11965812d 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -51,8 +51,6 @@ val w_Declare : env -> evar -> types -> evar_defs -> evar_defs (***********************************************************) (* Instanciate evars *) -val w_Define : evar -> constr -> evar_defs -> evar_defs - (* suspicious env ? *) val evar_define : env -> existential -> constr -> evar_defs -> evar_defs * evar list diff --git a/pretyping/evd.ml b/pretyping/evd.ml index dbcfae0e8..d1d8d3817 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -49,15 +49,16 @@ let fold = Evarmap.fold let add evd ev newinfo = Evarmap.add ev newinfo evd let define evd ev body = - let oldinfo = map evd ev in + let oldinfo = + try map evd ev + with Not_found -> error "Evd.define: cannot define undeclared evar" in let newinfo = { evar_concl = oldinfo.evar_concl; evar_hyps = oldinfo.evar_hyps; - evar_body = Evar_defined body} - in + evar_body = Evar_defined body} in match oldinfo.evar_body with | Evar_empty -> Evarmap.add ev newinfo evd - | _ -> anomaly "cannot define an isevar twice" + | _ -> anomaly "Evd.define: cannot define an isevar twice" let is_evar sigma ev = in_dom sigma ev diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 2801d3ee4..0c5d7d672 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -267,8 +267,8 @@ let w_merge env with_types mod_delta metas evars evd = (Retyping.get_type_of sp_env (evars_of evd') c) ev.evar_concl in let evd'' = w_merge_rec evd' mc ec in if (evars_of evd') == (evars_of evd'') - then w_Define sp c evd'' - else w_Define sp (Evarutil.nf_evar (evars_of evd'') c) evd'' in + then Evd.evar_define sp c evd'' + else Evd.evar_define sp (Evarutil.nf_evar (evars_of evd'') c) evd'' in (* merge constraints *) let evd' = w_merge_rec evd metas evars in |