diff options
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 *) |