aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3938.v
blob: 859e9f01776945ee551372bcafe2d13bc8151f35 (plain)
1
2
3
4
5
6
7
8
Require Import TestSuite.admit.
Require Import Coq.Arith.PeanoNat.
Hint Extern 1 => admit : typeclass_instances.
Require Import Setoid.
Goal forall a b (f : nat -> Set) (R : nat -> nat -> Prop), 
       Equivalence R -> R a b -> f a = f b.
  intros a b f H.
  intros. Fail rewrite H1.