diff options
| -rw-r--r-- | pretyping/clenv.ml | 2 | ||||
| -rw-r--r-- | pretyping/evd.mli | 4 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 14 |
4 files changed, 14 insertions, 7 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 4b5e40408..d21c8ad45 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 07706c0ba..bcada1fc0 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 *) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index bdc1f6b66..ff7cf5acc 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -70,7 +70,6 @@ let clenv_pose_dependent_evars with_evars clenv = (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); clenv_pose_metas_as_evars clenv dep_mvs - let clenv_refine with_evars ?(with_classes=true) clenv gls = let clenv = clenv_pose_dependent_evars with_evars clenv in let evd' = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 7796c36fb..8e920ef64 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -837,8 +837,14 @@ let check_evars sigma evm gl = evm Evd.empty in if rest <> Evd.empty then - errorlabstrm "apply" (str"Uninstantiated existential variables: " ++ - fnl () ++ pr_evar_defs rest) + errorlabstrm "apply" (str"Uninstantiated existential "++ + str(plural (List.length (Evd.to_list rest)) "variable")++str": " ++ + fnl () ++ pr_evar_defs rest);; + +let get_bindings_evars = function + | ImplicitBindings largs -> List.map fst largs + | ExplicitBindings lbind -> List.map (fun x -> fst (pi3 x)) lbind + | NoBindings -> [] let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 = let flags = @@ -847,7 +853,8 @@ let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 = goal. If this fails, then the head constant will be unfolded step by step. *) let concl_nprod = nb_prod (pf_concl gl0) in - let evm, c = c in + let evmc, c = c in + let evm = List.fold_left Evd.merge evmc (get_bindings_evars lbind) in let rec try_main_apply with_destruct c gl = let thm_ty0 = nf_betaiota (project gl) (pf_type_of gl c) in let try_apply thm_ty nprod = @@ -950,6 +957,7 @@ let apply_in_once with_delta with_destruct with_evars id (loc,((sigma,d),lbind)) gl0 = let flags = if with_delta then default_unify_flags else default_no_delta_unify_flags in + let sigma = List.fold_left Evd.merge sigma (get_bindings_evars lbind) in let t' = pf_get_hyp_typ gl0 id in let innerclause = mk_clenv_from_n gl0 (Some 0) (mkVar id,t') in let rec aux with_destruct c gl = |