diff options
| author | herbelin | 2009-09-18 18:58:18 +0000 |
|---|---|---|
| committer | herbelin | 2009-09-18 18:58:18 +0000 |
| commit | 3341fdc330f65af15a23f97620978a7e04e78d01 (patch) | |
| tree | 0ef19aed195239afa85eeb7d284087384300c37e /pretyping | |
| parent | a537c9f47ac6be8ecbbef284206869136e43f00b (diff) | |
- Fixed a bug in checking that implicit arguments are all correctly
instantiated in tactics (here apply and apply in) that should not open
existential goals (see Bas Spitters' coq-club mail about "exists" leaving
open existentials).
- Preserved the history of the evars occurring in bindings.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12345 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/clenv.ml | 2 | ||||
| -rw-r--r-- | pretyping/evd.mli | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 4b5e40408d..d21c8ad45a 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -409,7 +409,7 @@ let clenv_unify_binding_type clenv c t u = let clenv_assign_binding clenv k (sigma,c) = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in - let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in + let clenv' = { clenv with evd = Evd.merge clenv.evd sigma} in let c_typ = nf_betaiota clenv'.evd (clenv_get_type_of clenv' c) in let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd } diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 07706c0ba4..bcada1fc00 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -187,8 +187,8 @@ val evar_declare : ?filter:bool list -> evar_defs -> evar_defs val evar_source : existential_key -> evar_defs -> loc * hole_kind -(* spiwack: this function seesm to somewhat break the abstraction. *) -(* [evar_merge evd evars] extends the evars of [evd] with [evars] *) +(* spiwack: this function seems to somewhat break the abstraction. *) +(* [evar_merge evd ev1] extends the evars of [evd] with [evd1] *) val evar_merge : evar_defs -> evar_defs -> evar_defs (* Unification constraints *) |