diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-01-05 12:57:56 +0100 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-01-05 15:34:23 +0100 |
| commit | 3a447d83226c4591e796e44933dad8278d97d683 (patch) | |
| tree | 7c6f452b7bc4900d22767d005b0b3d29f07c83fd /vernac/vernacentries.ml | |
| parent | 2d6e395dead61a49ede6208bc40e16b4b8e68ce4 (diff) | |
Brackets support single numbered goal selectors.
This allows to focus on a sub-goal other than the first one without
resorting to the `Focus` command.
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index ded0d97e6..bccde169f 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1846,11 +1846,8 @@ let vernac_unfocused () = user_err Pp.(str "The proof is not fully unfocused.") -(* BeginSubproof / EndSubproof. - BeginSubproof (vernac_subproof) focuses on the first goal, or the goal - given as argument. - EndSubproof (vernac_end_subproof) unfocuses from a BeginSubproof, provided - that the proof of the goal has been completed. +(* "{" focuses on the first goal, "n: {" focuses on the n-th goal + "}" unfocuses, provided that the proof of the goal has been completed. *) let subproof_kind = Proof.new_focus_kind () let subproof_cond = Proof.done_cond subproof_kind @@ -1859,7 +1856,9 @@ let vernac_subproof gln = Proof_global.simple_with_current_proof (fun _ p -> match gln with | None -> Proof.focus subproof_cond () 1 p - | Some n -> Proof.focus subproof_cond () n p) + | Some (SelectNth n) -> Proof.focus subproof_cond () n p + | _ -> user_err ~hdr:"bracket_selector" + (str "Brackets only support the single numbered goal selector.")) let vernac_end_subproof () = Proof_global.simple_with_current_proof (fun _ p -> |