- 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

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 =