blob: 5b326e389b2c3465abed99fe85674ee38d75195e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
(* -*- coq-prog-args: ("-noinit"); -*- *)
Unset Elimination Schemes.
Module Type S.
Inductive foo : Prop :=.
Definition bar (x:foo) : Prop := match x with end.
End S.
Module M.
Inductive foo : Prop :=.
Definition bar (x:foo) : Prop := match x with end.
End M.
Module MS : S := M.
Module F (Z:S) := Z.
Module MS' : S := F M.
|
