diff options
| author | aspiwack | 2012-03-30 12:51:23 +0000 |
|---|---|---|
| committer | aspiwack | 2012-03-30 12:51:23 +0000 |
| commit | c2c41a164c5eecc62995752ec9e22904cf7e7cd1 (patch) | |
| tree | 7c9f9a707f0906ce0fb21b16188e29bd425a851e /toplevel | |
| parent | 1e1b6828c29b1344f50f94f9d3a6fce27a885656 (diff) | |
Added a command "Unfocused" which returns an error when the proof is
not fully unfocused (in the style of the Guarded command).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15104 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 10 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 1 |
2 files changed, 11 insertions, 0 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2e01aa3ea7..355e693569 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1412,6 +1412,15 @@ let vernac_unfocus () = let p = Proof_global.give_me_the_proof () in Proof.unfocus command_focus p; print_subgoals () +(* Checks that a proof is fully unfocused. Raises an error if not. *) +let vernac_unfocused () = + let p = Proof_global.give_me_the_proof () in + if Proof.unfocused p then + msg (str"The proof is indeed fully unfocused.") + else + error "The proof is not fully unfocused." + + (* BeginSubproof / EndSubproof. BeginSubproof (vernac_subproof) focuses on the first goal, or the goal given as argument. @@ -1591,6 +1600,7 @@ let interp c = match c with | VernacBacktrack (snum,pnum,naborts) -> vernac_backtrack snum pnum naborts | VernacFocus n -> vernac_focus n | VernacUnfocus -> vernac_unfocus () + | VernacUnfocused -> vernac_unfocused () | VernacBullet b -> vernac_bullet b | VernacSubproof n -> vernac_subproof n | VernacEndSubproof -> vernac_end_subproof () diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 7fecdb8a34..e9ecc95ecb 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -350,6 +350,7 @@ type vernac_expr = | VernacBacktrack of int*int*int | VernacFocus of int option | VernacUnfocus + | VernacUnfocused | VernacBullet of bullet | VernacSubproof of int option | VernacEndSubproof |