diff options
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/autorewrite.v (renamed from test-suite/success/autorewritein.v) | 6 | ||||
| -rw-r--r-- | test-suite/success/rewrite.v | 11 |
2 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/success/autorewritein.v b/test-suite/success/autorewrite.v index 68f2f7ce73..5e9064f8af 100644 --- a/test-suite/success/autorewritein.v +++ b/test-suite/success/autorewrite.v @@ -19,5 +19,11 @@ Proof. apply H;reflexivity. Qed. +(* Check autorewrite does not solve existing evars *) +(* See discussion started by A. Chargueraud in Oct 2010 on coqdev *) +Hint Rewrite <- plus_n_O : base1. +Goal forall y, exists x, y+x = y. +eexists. autorewrite with base1. +Fail reflexivity. diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index 3bce52fe78..3d49d3cf93 100644 --- a/test-suite/success/rewrite.v +++ b/test-suite/success/rewrite.v @@ -108,3 +108,14 @@ 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. + |