blob: 732a024fc16fa0293ae0302de8678e08bdf11445 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(* -*- coq-prog-args: ("-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.
|