aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/opened/3938.v
blob: 2d0d1930f1fca3df7aaf7c4b3998703e2489ffdb (plain)
1
2
3
4
5
6
Require Import Coq.Arith.PeanoNat.
Hint Extern 1 => admit : typeclass_instances.
Goal forall a b (f : nat -> Set), Nat.eq a b -> f a = f b.
  intros a b f H.
  rewrite H. (* Toplevel input, characters 15-25:
Anomaly: Evar ?X11 was not declared. Please report. *)