blob: 7abc38bfceec006ddc4dacac4371aabcab4c2da3 (
plain)
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.
|