Reactivation of pattern unification of evars in apply unification, in

agreement with wish #2117 (pattern unification of evars remained
deactivated for 3 years because of incompatibilities with eauto [see
commit 9234]; thanks to unification flags, it can be activated for
apply w/o changing eauto).
Also add test for bug #2123 (see commit 12228).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12229 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 34 insertions, 2 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 8ea2eae11..0846359a8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -128,6 +128,7 @@ type unify_flags = {
   use_metas_eagerly : bool;
   modulo_delta : Names.transparent_state;
   resolve_evars : bool;
+  use_evars_pattern_unification : bool
 }
 
 let default_unify_flags = {
@@ -135,6 +136,7 @@ let default_unify_flags = {
   use_metas_eagerly = true;
   modulo_delta = full_transparent_state;
   resolve_evars = false;
+  use_evars_pattern_unification = true;
 }
 
 let default_no_delta_unify_flags = {
@@ -142,6 +144,7 @@ let default_no_delta_unify_flags = {
   use_metas_eagerly = true;
   modulo_delta = empty_transparent_state;
   resolve_evars = false;
+  use_evars_pattern_unification = true;
 }
 
 let expand_key env = function
@@ -229,12 +232,14 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 		  (unirec_rec curenvnb topconv true substn p1 p2) c1 c2) cl1 cl2
 
 	| App (f1,l1), _ when
-	    isMeta f1 & is_unification_pattern curenvnb f1 l1 cN &
+	    (isMeta f1 || flags.use_evars_pattern_unification && isEvar f1) &
+	    is_unification_pattern curenvnb f1 l1 cN &
 	    not (dependent f1 cN) ->
 	      solve_pattern_eqn_array curenvnb f1 l1 cN substn
 
 	| _, App (f2,l2) when
-	    isMeta f2 & is_unification_pattern curenvnb f2 l2 cM &
+	    (isMeta f2 || flags.use_evars_pattern_unification && isEvar f2) &
+	    is_unification_pattern curenvnb f2 l2 cM &
 	    not (dependent f2 cM) ->
 	      solve_pattern_eqn_array curenvnb f2 l2 cM substn
 
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 8d71ec4bd..43c9dd2e9 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -19,6 +19,7 @@ type unify_flags = {
   use_metas_eagerly : bool;
   modulo_delta : Names.transparent_state;
   resolve_evars : bool;
+  use_evars_pattern_unification : bool
 }
 
 val default_unify_flags : unify_flags
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index c3e6e3d87..87dd26779 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -109,6 +109,7 @@ let fail_quick_unif_flags = {
   use_metas_eagerly = false;
   modulo_delta = empty_transparent_state;
   resolve_evars = false;
+  use_evars_pattern_unification = false;
 }
 
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 8a2578c30..407733e68 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -709,6 +709,7 @@ let auto_unif_flags = {
   use_metas_eagerly = false;
   modulo_delta = empty_transparent_state;
   resolve_evars = true;
+  use_evars_pattern_unification = false;
 }
 
 (* Try unification with the precompiled clause, then use registered Apply *)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 6baedb76a..2b9a48030 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -104,6 +104,7 @@ let auto_unif_flags = {
   use_metas_eagerly = true;
   modulo_delta = var_full_transparent_state;
   resolve_evars = false;
+  use_evars_pattern_unification = true;
 }
 
 let unify_e_resolve flags (c,clenv) gls = 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index dcb2d6037..89a3704ee 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -66,6 +66,7 @@ let rewrite_unif_flags = {
   Unification.use_metas_eagerly = true;
   Unification.modulo_delta = empty_transparent_state;
   Unification.resolve_evars = true;
+  Unification.use_evars_pattern_unification = true;
 }
 
 let side_tac tac sidetac =
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 6da110139..52f10d46c 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -283,6 +283,7 @@ let rewrite_unif_flags = {
   Unification.use_metas_eagerly = true;
   Unification.modulo_delta = empty_transparent_state;
   Unification.resolve_evars = true;
+  Unification.use_evars_pattern_unification = true;
 }
 
 let conv_transparent_state = (Idpred.empty, Cpred.full)
@@ -292,6 +293,7 @@ let rewrite2_unif_flags = {
   Unification.use_metas_eagerly = true;
   Unification.modulo_delta = empty_transparent_state;
   Unification.resolve_evars = true;
+  Unification.use_evars_pattern_unification = true;
 }
 
 let setoid_rewrite_unif_flags = {
@@ -299,6 +301,7 @@ let setoid_rewrite_unif_flags = {
   Unification.use_metas_eagerly = true;
   Unification.modulo_delta = conv_transparent_state;
   Unification.resolve_evars = true;
+  Unification.use_evars_pattern_unification = true;
 }
 
 let convertible env evd x y =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3cd819947..e96806de1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -681,6 +681,7 @@ let elim_flags = {
   use_metas_eagerly = true;
   modulo_delta = empty_transparent_state;
   resolve_evars = false;
+  use_evars_pattern_unification = true;
 }
 
 let elimination_clause_scheme with_evars allow_K elimclause indclause gl = 
diff --git a/test-suite/bugs/closed/shouldsucceed/2123.v b/test-suite/bugs/closed/shouldsucceed/2123.v
new file mode 100644
index 000000000..422a2c126
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2123.v
@@ -0,0 +1,11 @@
+(* About the detection of non-dependent metas by the refine tactic *)
+
+(* The following is a simplification of bug #2123 *)
+
+Parameter fset : nat -> Set.
+Parameter widen : forall (n : nat) (s : fset n), { x : fset (S n) | s=s }.
+Goal forall i, fset (S i).
+intro.
+refine (proj1_sig (widen i _)).
+
+
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 4f47702c6..f95352b65 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -277,3 +277,10 @@ try eapply ex_intro.
 trivial.
 Qed.
 
+(* Check pattern-unification on evars in apply unification *)
+
+Lemma evar : exists f : nat -> nat, forall x, f x = 0 -> x = 0.
+Proof.
+eexists; intros x H.
+apply H.
+Qed.