Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".

Noticed by Sigurd Schneider.

6 files changed, 29 insertions, 4 deletions

diff --git a/CHANGES b/CHANGES
index 2040c1b57..c164ed9b8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -54,6 +54,9 @@ Tactics
   with let bindings in the parameters.
 - The tactic "dtauto" now handles some inductives such as
   "@sigT A (fun _ => B)" as non-dependent conjunctions.
+- A bug fixed in "rewrite H in *" and "rewrite H in * |-" may cause a
+  few rare incompatibilities (it was unintendedly recursively
+  rewriting in the side conditions generated by H).
 
 Focusing
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 66a5f107a..bf30a3051 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2904,7 +2904,7 @@ This happens if \term$_1$ does not occur in the goal.
       rewrite H in H2 at - 2}. In particular a failure will happen if any of
     these three simpler tactics fails.
   \item \texttt{rewrite H in * |- } will do \texttt{rewrite H in
-      H$_i$} for all hypothesis \texttt{H$_i$ <> H}. A success will happen
+      H$_i$} for all hypotheses \texttt{H$_i$} different from \texttt{H}. A success will happen
     as soon as at least one of these simpler tactics succeeds.
   \item \texttt{rewrite H in *} is a combination of \texttt{rewrite H}
     and \texttt{rewrite H in * |-} that succeeds if at
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9a1ac768c..32563d9ff 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -533,7 +533,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
 	let rec do_hyps_atleastonce = function
 	  | [] -> tclZEROMSG (Pp.str"Nothing to rewrite.")
 	  | id :: l ->
-	    tclIFTHENTRYELSEMUST
+            tclIFTHENFIRSTTRYELSEMUST
 	     (general_rewrite_ebindings_in l2r AllOccurrences false true ?tac id c with_evars)
 	     (do_hyps_atleastonce l)
 	in
@@ -549,7 +549,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
           end
 	in
 	if cl.concl_occs == NoOccurrences then do_hyps else
-	  tclIFTHENTRYELSEMUST
+          tclIFTHENFIRSTTRYELSEMUST
 	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars)
 	   do_hyps
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index e7da17cff..0cc0001c1 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -408,8 +408,14 @@ module New = struct
     Proofview.tclIFCATCH t1
       (fun () -> tclDISPATCH (Array.to_list a))
       (fun _ -> t3)
+  let tclIFTHENFIRSTELSE t1 t2 t3 =
+    Proofview.tclIFCATCH t1
+      (fun () -> tclEXTEND [t2] (tclUNIT ()) [])
+      (fun _ -> t3)
   let tclIFTHENTRYELSEMUST t1 t2 =
     tclIFTHENELSE t1 (tclTRY t2) t2
+  let tclIFTHENFIRSTTRYELSEMUST t1 t2 =
+    tclIFTHENFIRSTELSE t1 (tclTRY t2) t2
 
   (* Try the first tactic that does not fail in a list of tactics *)
   let rec tclFIRST = function
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index c5d5c8c12..a3bc4707e 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -210,6 +210,7 @@ module New : sig
   val tclIFTHENELSE : unit tactic -> unit tactic -> unit tactic -> unit tactic
   val tclIFTHENSVELSE : unit tactic -> unit tactic array -> unit tactic -> unit tactic
   val tclIFTHENTRYELSEMUST : unit tactic -> unit tactic -> unit tactic
+  val tclIFTHENFIRSTTRYELSEMUST : unit tactic -> unit tactic -> unit tactic
 
   val tclDO : int -> unit tactic -> unit tactic
   val tclREPEAT : unit tactic -> unit tactic
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 62249666b..448d0082d 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -151,10 +151,25 @@ Abort.
 
 (* Check that rewriting within evars still work (was broken in 8.5beta1) *)
 
-
 Goal forall (a: unit) (H: a = tt), exists x y:nat, x = y.
 intros; eexists; eexists.
 rewrite H.
 Undo.
 subst.
 Abort.
+
+(* Check that iterated rewriting does not rewrite in the side conditions *)
+(* Example from Sigurd Schneider, extracted from contrib containers *)
+
+Lemma EQ
+  : forall (e e' : nat), True -> e = e'.
+Admitted.
+
+Lemma test (v1 v2 v3: nat) (v' : v1 = v2) : v2 = v1.
+Proof.
+  rewrite <- (EQ v1 v2) in *.
+  exact v'.
+  (* There should be only two side conditions *)
+  exact I.
+  exact I.
+Qed.