diff options
| author | msozeau | 2008-03-21 16:20:59 +0000 |
|---|---|---|
| committer | msozeau | 2008-03-21 16:20:59 +0000 |
| commit | 123c8683a25b34070d4874df4cdd9381d5ceac24 (patch) | |
| tree | 58b51cbd58bc8492d2b79985f917d49dccefd567 /pretyping | |
| parent | 78e8a11a5f40c5ee1c09e279350ab208c4a31b64 (diff) | |
Correct bug introduced in r10589, where we lost information that
assumption types are types when type-checking them and necessary
coercions were not inserted. Add empty_evar_defs definition in Evd and
call the new helper function in constrintern that performs
interpretation and gives back implicit argument information.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10706 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 1 | ||||
| -rw-r--r-- | pretyping/evd.mli | 1 |
2 files changed, 2 insertions, 0 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 |