blob: ede573a34ef80d6d7606048b5fd6e3e9f8294c36 (
plain)
1
2
3
4
5
6
7
8
9
|
(* Simplification of bug 711 *)
Parameter f : true = false.
Goal let p := f in True.
intro p.
set (b := true) in *.
(* Check that it doesn't fail with an anomaly *)
(* Ultimately, adapt destruct to make it succeeding *)
try destruct b.
|
