1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
(* Test regression https://github.com/coq/coq/issues/16140
where congruence produces ill-typed terms *)
Inductive wrap1 : Type :=
wrap1I (u : unit) : match u with tt => bool end -> wrap1.
Goal (wrap1I tt false) = (wrap1I tt true) -> False.
Proof.
Fail congruence. (* expected to fail *)
Abort.
Inductive wrap2 : unit -> Type :=
wrap2I (u : unit) : match u with tt => bool end -> wrap2 u.
Goal (wrap2I tt false) = (wrap2I tt true) -> False.
Proof.
Fail congruence. (* expected to fail *)
Abort.
Inductive wrap3 (u : unit) : Type :=
wrap3I : match u with tt => bool end -> wrap3 u.
Goal (wrap3I tt false) = (wrap3I tt true) -> False.
Proof.
congruence.
Qed.
|
