diff options
| -rw-r--r-- | pretyping/evd.ml | 1 | ||||
| -rw-r--r-- | pretyping/evd.mli | 1 | ||||
| -rw-r--r-- | toplevel/command.ml | 10 |
3 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index e044c17a99..2703e5ae0c 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -414,6 +414,7 @@ let create_evar_defs sigma = let create_goal_evar_defs sigma = let h = fold (fun mv _ l -> (mv,(dummy_loc,GoalEvar))::l) sigma [] in { evars=sigma; conv_pbs=[]; last_mods = []; history=h; metas=Metamap.empty } +let empty_evar_defs = create_evar_defs empty let evars_of d = d.evars let evars_reset_evd evd d = {d with evars = evd} let reset_evd (sigma,mmap) d = {d with evars = sigma; metas=mmap} diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 7f5a4060b1..ebda685bd6 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -143,6 +143,7 @@ val subst_evar_defs_light : substitution -> evar_defs -> evar_defs (* create an [evar_defs] with empty meta map: *) val create_evar_defs : evar_map -> evar_defs val create_goal_evar_defs : evar_map -> evar_defs +val empty_evar_defs : evar_defs val evars_of : evar_defs -> evar_map val evars_reset_evd : evar_map -> evar_defs -> evar_defs diff --git a/toplevel/command.ml b/toplevel/command.ml index f4887ae4d8..fa206e7451 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -205,12 +205,10 @@ let set_declare_assumption_hook = (:=) declare_assumption_hook let declare_assumption idl is_coe k bl c nl= if not (Pfedit.refining ()) then let c = generalize_constr_expr c bl in - let sigma = Evd.empty and env = Global.env () in - let ic = intern_type sigma env c in - let imps = Implicit_quantifiers.implicits_of_rawterm ic in - let j = Default.understand_judgment sigma env ic in - !declare_assumption_hook j.uj_val; - List.iter (declare_one_assumption is_coe k j.uj_val imps nl) idl + let sigma = ref Evd.empty_evar_defs and env = Global.env () in + let c', imps = interp_type_evars_impls sigma env c in + !declare_assumption_hook c'; + List.iter (declare_one_assumption is_coe k c' imps nl) idl else errorlabstrm "Command.Assumption" (str "Cannot declare an assumption while in proof editing mode.") |