aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4679.v
blob: c94fa31a9da1014d774610a78b37b7351d6d0326 (plain)
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.