blob: db6348fa171806e4b94234f398bfe697745e4fdb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
Goal True.
solve [ constructor 1 ]. Undo.
solve [ econstructor 1 ]. Undo.
solve [ constructor ]. Undo.
solve [ econstructor ]. Undo.
solve [ constructor (fail) ]. Undo.
solve [ econstructor (fail) ]. Undo.
split.
Qed.
Goal False \/ True.
solve [ constructor (constructor) ]. Undo.
solve [ econstructor (econstructor) ]. Undo.
solve [ constructor 2; constructor ]. Undo.
solve [ econstructor 2; econstructor ]. Undo.
right; esplit.
Qed.
|
