Granting Jason's request for an ad hoc compatibility option on

considering trivial unifications "?x = t" in tactics working under
conjunctions (see #3545).

Also updating and fixing wrong comments in test apply.v.

4 files changed, 58 insertions, 18 deletions

diff --git a/CHANGES b/CHANGES
index 2e5e30ef8d..08484a4b9b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -20,6 +20,9 @@ Tactics
   will eventually fail and backtrack.
   * "Strict" changes the behavior of an unloaded hint to the one of the fail
   tactic, allowing to emulate the hopefully future import-scoped hint mechanism.
+- New compatibility flag "Universal Lemma Under Conjunction" which
+  let tactics working under conjunctions apply sublemmas of the form
+  "forall A, ... -> A".
 
 API
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index cc262708ab..fa6f783934 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -485,7 +485,24 @@ apply Rmp.
 Reset R.
 \end{coq_eval}
 
+\noindent {\bf Remark: } When the conclusion of the type of the term
+to apply is an inductive type isomorphic to a tuple type and {\em apply}
+looks recursively whether a component of the tuple matches the goal,
+it excludes components whose statement would result in applying an
+universal lemma of the form {\tt forall A, ... -> A}. Excluding this
+kind of lemma can be avoided by setting the following option:
+
+\begin{quote}
+\optindex{Universal Lemma Under Conjunction}
+{\tt Set Universal Lemma Under Conjunction}
+\end{quote}
+
+This option, which preserves compatibility with versions of {\Coq}
+prior to 8.4 is also available for {\tt apply {\term} in {\ident}}
+(see Section~\ref{apply-in}).
+
 \subsection{\tt apply {\term} in {\ident}}
+\label{apply-in}
 \tacindex{apply \dots\ in}
 
 This tactic applies to any goal.  The argument {\term} is a term
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 402a9e88a1..6d81a48705 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -109,6 +109,24 @@ let _ =
       optread  = (fun () -> !clear_hyp_by_default) ;
       optwrite = (fun b -> clear_hyp_by_default := b) }
 
+(* Compatibility option useful in developments using apply intensively
+   in ltac code *)
+
+let universal_lemma_under_conjunctions = ref false
+
+let accept_universal_lemma_under_conjunctions () =
+  !universal_lemma_under_conjunctions
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "trivial unification in tactics applying under conjunctions";
+      optkey   = ["Universal";"Lemma";"Under";"Conjunction"];
+      optread  = (fun () -> !universal_lemma_under_conjunctions) ;
+      optwrite = (fun b -> universal_lemma_under_conjunctions := b) }
+
+
 (*********************************************)
 (*                 Tactics                   *)
 (*********************************************)
@@ -1332,7 +1350,7 @@ let make_projection env sigma params cstr sign elim i n c u =
 	(* to avoid surprising unifications, excludes flexible
 	projection types or lambda which will be instantiated by Meta/Evar *)
 	&& not (isEvar (fst (whd_betaiota_stack sigma t)))
-	&& not (isRel t && destRel t > n-i)
+	&& (accept_universal_lemma_under_conjunctions () || not (isRel t))
       then
         let t = lift (i+1-n) t in
 	let abselim = beta_applist (elim,params@[t;branch]) in
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index a4ed76c5a0..24d5cf8a99 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -333,13 +333,10 @@ exact (refl_equal 3).
 exact (refl_equal 4).
 Qed.
 
-(* From 12612, descent in conjunctions is more powerful *)
+(* From 12612, Dec 2009, descent in conjunctions is more powerful *)
 (* The following, which was failing badly in bug 1980, is now
    properly rejected, as descend in conjunctions builds an
-   ill-formed elimination from Prop to Type.
-
-   Added Aug 2014: why it fails is now that trivial unification ?x = goal is
-   rejected by the descent in conjunctions to avoid surprising results. *)
+   ill-formed elimination from Prop to the domain of ex which is in Type. *)
 
 Goal True.
 Fail eapply ex_intro.
@@ -351,28 +348,32 @@ Fail eapply (ex_intro _).
 exact I.
 Qed.
 
-(* Note: the following succeed directly (i.e. w/o "exact I") since
-   Aug 2014 since the descent in conjunction does not use a "cut"
-   anymore: the iota-redex is contracted and we get rid of the
-   uninstantiated evars
-
-   Is it good or not? Maybe it does not matter so much.
+(* No failure here, because the domain of ex is in Prop *)
 
 Goal True.
-eapply (ex_intro (fun _ => True) I).    
-exact I. (* Not needed since Aug 2014 *)
+eapply (ex_intro (fun _ => 0=0) I).
+reflexivity.
 Qed.
 
 Goal True.
-eapply (ex_intro (fun _ => True) I _).    
-exact I. (* Not needed since Aug 2014 *)
+eapply (ex_intro (fun _ => 0=0) I _).
+Unshelve. (* In 8.4:  Grab Existential Variables. *)
+reflexivity.
 Qed.
 
 Goal True.
 eapply (fun (A:Prop) (x:A) => conj I x).
-exact I. (* Not needed since Aug 2014 *)
+Unshelve. (* In 8.4: the goal ?A was there *)
+exact I.
 Qed.
-*)
+
+(* Testing compatibility mode with v8.4 *)
+
+Goal True.
+Fail eapply existT.
+Set Trivial Tactic Unification Under Conjunction.
+eapply existT.
+Abort.
 
 (* The following was not accepted from r12612 to r12657 *)
 
@@ -463,6 +464,7 @@ Abort.
 Goal forall H:0=0, H = H.
 intros.
 Fail apply eq_sym in H.
+Abort.
 
 (* Check that unresolved evars not originally present in goal prevent
    apply in to work*)