test-suite/bugs/closed/5277.v


1
2
3
4
5
6
7
8
9
10
11

(* Scheme Equality not robust wrt names *)

Module A1.
  Inductive A (T : Type) := C (a : T).
  Scheme Equality for A. (* success *)
End A1.

Module A2.
  Inductive A (x : Type) := C (a : x).
  Scheme Equality for A. 
End A2.