1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
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.
|
