diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-07-26 16:16:08 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-07-26 16:16:08 +0200 |
| commit | dc1db99e019242c07f00837f8316a8d392c40258 (patch) | |
| tree | ff271f3a63d9b4e7e6bf6bde4c590003c549c2c4 /test-suite | |
| parent | 139204928e55f92f02d3b3dd1d6746e34fdcdb88 (diff) | |
| parent | 1ca19082cf506c304b3c7945e72c0238f2aa9d1a (diff) | |
Merge branch 'v8.6' into trunk
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/4679.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4679.v b/test-suite/bugs/closed/4679.v new file mode 100644 index 000000000..c94fa31a9 --- /dev/null +++ b/test-suite/bugs/closed/4679.v @@ -0,0 +1,18 @@ +Require Import Coq.Setoids.Setoid. +Goal forall (T : nat -> Set -> Set) (U : Set) + (H : forall n : nat, T n (match n with + | 0 => fun x => x + | S _ => fun x => x + end (nat = nat)) = U), + T 0 (nat = nat) = U. +Proof. + intros. + let H := match goal with H : forall _, eq _ _ |- _ => H end in + rewrite H || fail 0 "too early". + Undo. + let H := match goal with H : forall _, eq _ _ |- _ => H end in + setoid_rewrite (H 0) || fail 0 "too early". + Undo. + setoid_rewrite H. (* Error: Tactic failure: setoid rewrite failed: Nothing to rewrite. *) + reflexivity. +Qed.
\ No newline at end of file |