diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
commit | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /test-suite/success/rewrite.v | |
parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) |
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'test-suite/success/rewrite.v')
-rw-r--r-- | test-suite/success/rewrite.v | 21 |
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. + |