Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 21 insertions, 0 deletions

diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 3bce52fe..08c406be 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -108,3 +108,24 @@ intros.
 rewrite (H _).
 reflexivity.
 Qed.
+
+(* Example of rewriting of a degenerated pattern using the right-most
+   argument of the goal. This is sometimes used in contribs, even if
+   ad hoc. Here, we have the extra requirement that checking types
+   needs delta-conversion *)
+
+Axiom s : forall (A B : Type) (p : A * B), p = (fst p, snd p).
+Definition P := (nat * nat)%type.
+Goal forall x:P, x = x.
+intros. rewrite s.
+Abort.
+
+(* Test second-order unification and failure of pattern-unification *)
+
+Goal forall (P: forall Y, Y -> Prop) Y a, Y = nat -> (True -> P Y a) -> False.
+intros.
+(* The next line used to succeed between June and November 2011 *)
+(* causing ill-typed rewriting *)
+Fail rewrite H in H0.
+Abort.
+