diff options
| -rw-r--r-- | CHANGES | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 9 | ||||
| -rw-r--r-- | ide/coq_lex.mll | 4 | ||||
| -rw-r--r-- | intf/vernacexpr.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_ltac.ml4 | 3 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 4 | ||||
| -rw-r--r-- | test-suite/success/BracketsWithGoalSelector.v | 16 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 11 |
8 files changed, 44 insertions, 11 deletions
@@ -41,6 +41,12 @@ Tactics Heap, which performs a major garbage collection and heap compaction in the OCaml run-time system. +Focusing + +- Focusing bracket `{` now supports single-numbered goal selector, + e.g. `2: {` will focus on the second sub-goal. As usual, unfocus + with `}` once the sub-goal is fully solved. + Vernacular Commands - The deprecated Coercion Local, Open Local Scope, Notation Local syntax diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 3d4c885b3..6b24fdde7 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -320,10 +320,19 @@ Note that when a focused goal is proved a message is displayed together with a suggestion about the right bullet or {\tt \}} to unfocus it or focus the next one. +\begin{Variants} + +\item {\tt {\num}: \{}\\ +This focuses on the $\num^{th}$ subgoal to prove. + +\end{Variants} + \begin{ErrMsgs} \item \errindex{This proof is focused, but cannot be unfocused this way} You are trying to use {\tt \}} but the current subproof has not been fully solved. +\item \errindex{No such goal} +\item \errindex{Brackets only support the single numbered goal selector} \item see also error message about bullets below. \end{ErrMsgs} diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index 8bfd937e3..a7e9003db 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -17,7 +17,9 @@ let space = [' ' '\n' '\r' '\t' '\012'] (* '\012' is form-feed *) -let undotted_sep = '{' | '}' | '-'+ | '+'+ | '*'+ +let number = [ '0'-'9' ]+ + +let undotted_sep = (number space* ':' space*)? '{' | '}' | '-'+ | '+'+ | '*'+ let dot_sep = '.' (space | eof) diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 5106e513b..bc7b0585d 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -451,7 +451,7 @@ type vernac_expr = | VernacUnfocus | VernacUnfocused | VernacBullet of bullet - | VernacSubproof of int option + | VernacSubproof of goal_selector option | VernacEndSubproof | VernacShow of showable | VernacCheckGuard diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index ebf6e450b..cc7ce339b 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -327,7 +327,8 @@ GEXTEND Gram | IDENT "all"; ":" -> SelectAll ] ] ; tactic_mode: - [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g ] ] + [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g + | g = OPT toplevel_selector; "{" -> Vernacexpr.VernacSubproof g ] ] ; command: [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index e88284fb1..27c46fe4e 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -91,7 +91,7 @@ open Decl_kinds let sep_end = function | VernacBullet _ - | VernacSubproof None + | VernacSubproof _ | VernacEndSubproof -> str"" | _ -> str"." @@ -1199,7 +1199,7 @@ open Decl_kinds | VernacSubproof None -> return (str "{") | VernacSubproof (Some i) -> - return (keyword "BeginSubproof" ++ spc () ++ int i) + return (Proof_bullet.pr_goal_selector i ++ str ":" ++ spc () ++ str "{") | VernacEndSubproof -> return (str "}") diff --git a/test-suite/success/BracketsWithGoalSelector.v b/test-suite/success/BracketsWithGoalSelector.v new file mode 100644 index 000000000..ed035f521 --- /dev/null +++ b/test-suite/success/BracketsWithGoalSelector.v @@ -0,0 +1,16 @@ +Goal forall A B, B \/ A -> A \/ B. +Proof. + intros * [HB | HA]. + 2: { + left. + exact HA. + Fail right. (* No such goal. Try unfocusing with "}". *) + } + Fail 2: { (* Non-existent goal. *) + idtac. (* The idtac is to get a dot, so that IDEs know to stop there. *) + 1:{ (* Syntactic test: no space before bracket. *) + right. + exact HB. +Fail Qed. + } +Qed. 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 -> |