aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES6
-rw-r--r--Makefile.checker5
-rw-r--r--configure.ml9
-rw-r--r--dev/ocamldebug-coq.run2
-rw-r--r--doc/refman/RefMan-pro.tex9
-rw-r--r--ide/coq_lex.mll4
-rw-r--r--intf/vernacexpr.ml32
-rw-r--r--parsing/g_vernac.ml432
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--plugins/ltac/g_ltac.ml43
-rw-r--r--plugins/ssr/ssrvernac.ml44
-rw-r--r--printing/ppvernac.ml57
-rw-r--r--stm/proofBlockDelimiter.ml4
-rw-r--r--stm/stm.ml9
-rw-r--r--stm/vernac_classifier.ml14
-rw-r--r--test-suite/success/BracketsWithGoalSelector.v16
-rw-r--r--tools/md5sum.ml24
-rw-r--r--vernac/vernacentries.ml67
-rw-r--r--vernac/vernacinterp.ml1
-rw-r--r--vernac/vernacinterp.mli1
-rw-r--r--vernac/vernacprop.ml8
22 files changed, 181 insertions, 132 deletions
diff --git a/CHANGES b/CHANGES
index ead751147a..289b7d5d2d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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/Makefile.checker b/Makefile.checker
index 8334b6a2a6..0e429fe868 100644
--- a/Makefile.checker
+++ b/Makefile.checker
@@ -77,9 +77,8 @@ checker/%.cmx: checker/%.ml
md5chk:
$(SHOW)'MD5SUM cic.mli'
- $(HIDE)v=`tr -d "\r" < checker/cic.mli | $(MD5SUM) | sed -n -e 's/ .*//' -e '/^/p'`; \
- if grep -q "$$v" checker/values.ml; \
- then true; else echo "Error: outdated checker/values.ml: $$v" >&2; false; fi
+ $(HIDE)if grep -q "^MD5 $$($(OCAML) tools/md5sum.ml checker/cic.mli)$$" checker/values.ml; \
+ then true; else echo "Error: outdated checker/values.ml" >&2; false; fi
.PHONY: md5chk
diff --git a/configure.ml b/configure.ml
index e991eadace..ff767d96b4 100644
--- a/configure.ml
+++ b/configure.ml
@@ -861,13 +861,6 @@ let strip =
if strip = "" then "strip" else strip
end
-(** * md5sum command *)
-
-let md5sum =
- select_command "Don’t know how to compute MD5 checksums…" [
- "md5sum", [], [ "--version" ];
- "md5", ["-q"], [ "-s" ; "''" ];
- ]
(** * Documentation : do we have latex, hevea, ... *)
@@ -1246,8 +1239,6 @@ let write_makefile f =
pr "# Unix systems and profiling: true\n";
pr "# Unix systems and no profiling: strip\n";
pr "STRIP=%s\n\n" strip;
- pr "#the command md5sum\n";
- pr "MD5SUM=%s\n\n" md5sum;
pr "# LablGTK\n";
pr "COQIDEINCLUDES=%s\n\n" !lablgtkincludes;
pr "# CoqIde (no/byte/opt)\n";
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 3850c05fd9..3cbccab44c 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -17,7 +17,7 @@ export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH
exec $OCAMLDEBUG \
-I $CAMLP4LIB -I +threads \
-I $COQTOP \
- -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \
+ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \
-I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
-I $COQTOP/library -I $COQTOP/engine \
-I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 3d4c885b3a..6b24fdde79 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 8bfd937e38..a7e9003dbe 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 5106e513b9..8bd2da2f11 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -314,7 +314,16 @@ type cumulative_inductive_parsing_flag =
(** {6 The type of vernacular expressions} *)
-type vernac_expr =
+type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit
+
+type vernac_argument_status = {
+ name : Name.t;
+ recarg_like : bool;
+ notation_scope : string Loc.located option;
+ implicit_status : vernac_implicit_status;
+}
+
+type nonrec vernac_expr =
| VernacLoad of verbose_flag * string
(* Syntax *)
@@ -451,7 +460,7 @@ type vernac_expr =
| VernacUnfocus
| VernacUnfocused
| VernacBullet of bullet
- | VernacSubproof of int option
+ | VernacSubproof of goal_selector option
| VernacEndSubproof
| VernacShow of showable
| VernacCheckGuard
@@ -463,22 +472,13 @@ type vernac_expr =
(* For extension *)
| VernacExtend of extend_name * Genarg.raw_generic_argument list
- (* Flags *)
- | VernacProgram of vernac_expr
- | VernacPolymorphic of bool * vernac_expr
- | VernacLocal of bool * vernac_expr
-
-and vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit
-
-and vernac_argument_status = {
- name : Name.t;
- recarg_like : bool;
- notation_scope : string Loc.located option;
- implicit_status : vernac_implicit_status;
-}
+type nonrec vernac_flag =
+ | VernacProgram
+ | VernacPolymorphic of bool
+ | VernacLocal of bool
type vernac_control =
- | VernacExpr of vernac_expr
+ | VernacExpr of vernac_flag list * vernac_expr
(* boolean is true when the `-time` batch-mode command line flag was set.
the flag is used to print differently in `-time` vs `Time foo` *)
| VernacTime of bool * vernac_control located
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 92e60f4656..d498bda341 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -72,36 +72,36 @@ GEXTEND Gram
| IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c)
| IDENT "Timeout"; n = natural; v = vernac_control -> VernacTimeout(n,v)
| IDENT "Fail"; v = vernac_control -> VernacFail v
- | v = vernac -> VernacExpr(v) ]
+ | (f, v) = vernac -> VernacExpr(f, v) ]
]
;
vernac:
- [ [ IDENT "Local"; v = vernac_poly -> VernacLocal (true, v)
- | IDENT "Global"; v = vernac_poly -> VernacLocal (false, v)
+ [ [ IDENT "Local"; (f, v) = vernac_poly -> (VernacLocal true :: f, v)
+ | IDENT "Global"; (f, v) = vernac_poly -> (VernacLocal false :: f, v)
| v = vernac_poly -> v ]
]
;
vernac_poly:
- [ [ IDENT "Polymorphic"; v = vernac_aux -> VernacPolymorphic (true, v)
- | IDENT "Monomorphic"; v = vernac_aux -> VernacPolymorphic (false, v)
+ [ [ IDENT "Polymorphic"; (f, v) = vernac_aux -> (VernacPolymorphic true :: f, v)
+ | IDENT "Monomorphic"; (f, v) = vernac_aux -> (VernacPolymorphic false :: f, v)
| v = vernac_aux -> v ]
]
;
vernac_aux:
(* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
(* "." is still in the stream and discard_to_dot works correctly *)
- [ [ IDENT "Program"; g = gallina; "." -> VernacProgram g
- | IDENT "Program"; g = gallina_ext; "." -> VernacProgram g
- | g = gallina; "." -> g
- | g = gallina_ext; "." -> g
- | c = command; "." -> c
- | c = syntax; "." -> c
- | c = subprf -> c
+ [ [ IDENT "Program"; g = gallina; "." -> ([VernacProgram], g)
+ | IDENT "Program"; g = gallina_ext; "." -> ([VernacProgram], g)
+ | g = gallina; "." -> ([], g)
+ | g = gallina_ext; "." -> ([], g)
+ | c = command; "." -> ([], c)
+ | c = syntax; "." -> ([], c)
+ | c = subprf -> ([], c)
] ]
;
vernac_aux: LAST
- [ [ prfcom = command_entry -> prfcom ] ]
+ [ [ prfcom = command_entry -> ([], prfcom) ] ]
;
noedit_mode:
[ [ c = query_command -> c None] ]
@@ -621,11 +621,9 @@ GEXTEND Gram
VernacCanonical (AN qid)
| IDENT "Canonical"; IDENT "Structure"; ntn = by_notation ->
VernacCanonical (ByNotation ntn)
- | IDENT "Canonical"; IDENT "Structure"; qid = global;
- d = def_body ->
+ | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
let s = coerce_reference_to_id qid in
- VernacLocal(false,
- VernacDefinition ((NoDischarge,CanonicalStructure),((Loc.tag s),None),d))
+ VernacDefinition ((NoDischarge,CanonicalStructure),((Loc.tag s),None),d)
(* Coercions *)
| IDENT "Coercion"; qid = global; d = def_body ->
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 2fd6f53c4a..4b828a7022 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -154,7 +154,7 @@ VERNAC COMMAND EXTEND Function
| _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in
match
Vernac_classifier.classify_vernac
- (Vernacexpr.(VernacExpr(VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
+ (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
with
| Vernacexpr.VtSideff ids, _ when hard ->
Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index b4e17c5d1c..0b929b8ca9 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1509,7 +1509,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
+ Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
++ fnl () ++
msg
in
@@ -1524,7 +1524,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac Vernacexpr.(VernacExpr(VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
+ Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds)))
++ fnl () ++
CErrors.print reraise
in
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index ebf6e450b1..cc7ce339b2 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/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 4f530a0aec..c0479dd24b 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -551,9 +551,9 @@ GEXTEND Gram
| IDENT "Canonical"; qid = Constr.global;
d = G_vernac.def_body ->
let s = coerce_reference_to_id qid in
- Vernacexpr.VernacLocal(false,Vernacexpr.VernacDefinition
+ Vernacexpr.VernacDefinition
((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure),
- ((Loc.tag s),None),(d )))
+ ((Loc.tag s),None), d)
]];
END
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index e88284fb1c..96e39e89a6 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"."
@@ -535,17 +535,25 @@ open Decl_kinds
| SsFwdClose e -> "("^aux e^")*"
in Pp.str (aux e)
- let rec pr_vernac_expr v =
+ let pr_extend s cl =
+ let pr_arg a =
+ try pr_gen a
+ with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in
+ try
+ let rl = Egramml.get_extend_vernac_rule s in
+ let rec aux rl cl =
+ match rl, cl with
+ | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl
+ | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl
+ | [], [] -> []
+ | _ -> assert false in
+ hov 1 (pr_sequence identity (aux rl cl))
+ with Not_found ->
+ hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")
+
+ let pr_vernac_expr v =
let return = tag_vernac v in
match v with
- | VernacPolymorphic (poly, v) ->
- let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in
- return (s ++ spc () ++ pr_vernac_expr v)
- | VernacProgram v ->
- return (keyword "Program" ++ spc() ++ pr_vernac_expr v)
- | VernacLocal (local, v) ->
- return (pr_locality local ++ spc() ++ pr_vernac_expr v)
-
| VernacLoad (f,s) ->
return (
keyword "Load"
@@ -1199,30 +1207,25 @@ 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 "}")
- and pr_extend s cl =
- let pr_arg a =
- try pr_gen a
- with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in
- try
- let rl = Egramml.get_extend_vernac_rule s in
- let rec aux rl cl =
- match rl, cl with
- | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl
- | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl
- | [], [] -> []
- | _ -> assert false in
- hov 1 (pr_sequence identity (aux rl cl))
- with Not_found ->
- hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")
+let pr_vernac_flag =
+ function
+ | VernacPolymorphic true -> keyword "Polymorphic"
+ | VernacPolymorphic false -> keyword "Monomorphic"
+ | VernacProgram -> keyword "Program"
+ | VernacLocal local -> pr_locality local
let rec pr_vernac_control v =
let return = tag_vernac v in
match v with
- | VernacExpr v' -> pr_vernac_expr v' ++ sep_end v'
+ | VernacExpr (f, v') ->
+ List.fold_right
+ (fun f a -> pr_vernac_flag f ++ spc() ++ a)
+ f
+ (pr_vernac_expr v' ++ sep_end v')
| VernacTime (_,(_,v)) ->
return (keyword "Time" ++ spc() ++ pr_vernac_control v)
| VernacRedirect (s, (_,v)) ->
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 01b5b9a016..bebc4d5d5f 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -96,7 +96,7 @@ let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } =
`ValidBlock {
base_state = id;
goals_to_admit = focused;
- recovery_command = Some (Vernacexpr.VernacExpr(Vernacexpr.VernacBullet (to_bullet_val b)))
+ recovery_command = Some (Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b)))
}
| `Not -> `Leaks
@@ -125,7 +125,7 @@ let dynamic_curly_brace doc { dynamic_switch = id } =
`ValidBlock {
base_state = id;
goals_to_admit = focused;
- recovery_command = Some (Vernacexpr.VernacExpr Vernacexpr.VernacEndSubproof)
+ recovery_command = Some (Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof))
}
| `Not -> `Leaks
diff --git a/stm/stm.ml b/stm/stm.ml
index 7045df0ed2..5f4fe6565d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1498,7 +1498,7 @@ end = struct (* {{{ *)
stm_vernac_interp stop
~proof:(pobject, terminator) st
{ verbose = false; loc; indentation = 0; strlen = 0;
- expr = VernacExpr (VernacEndProof (Proved (Opaque,None))) }) in
+ expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) }) in
ignore(Future.join checked_proof);
end;
(* STATE: Restore the state XXX: handle exn *)
@@ -1646,7 +1646,7 @@ end = struct (* {{{ *)
let st = Vernacstate.freeze_interp_state `No in
ignore(stm_vernac_interp stop ~proof st
{ verbose = false; loc; indentation = 0; strlen = 0;
- expr = VernacExpr (VernacEndProof (Proved (Opaque,None))) });
+ expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) });
`OK proof
end
with e ->
@@ -2177,7 +2177,7 @@ let collect_proof keep cur hd brkind id =
(try
let name, hint = name ids, get_hint_ctx loc in
let t, v = proof_no_using last in
- v.expr <- VernacExpr(VernacProof(t, Some hint));
+ v.expr <- VernacExpr([], VernacProof(t, Some hint));
`ASync (parent last,accn,name,delegate name)
with Not_found ->
let name = name ids in
@@ -2872,10 +2872,9 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
if not in_proof && Proof_global.there_are_pending_proofs () then
begin
let bname = VCS.mk_branch_name x in
- let rec opacity_of_produced_term = function
+ let opacity_of_produced_term = function
(* This AST is ambiguous, hence we check it dynamically *)
| VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity
- | VernacLocal (_,e) -> opacity_of_produced_term e
| _ -> Doesn'tGuaranteeOpacity in
VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[]));
let proof_mode = default_proof_mode () in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 2fa47ba434..99b56d4846 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -49,17 +49,13 @@ let declare_vernac_classifier
classifiers := !classifiers @ [s,f]
let classify_vernac e =
- let rec static_classifier ~poly e = match e with
+ let static_classifier ~poly e = match e with
(* Univ poly compatibility: we run it now, so that we can just
* look at Flags in stm.ml. Would be nicer to have the stm
* look at the entire dag to detect this option. *)
| ( VernacSetOption (l,_) | VernacUnsetOption l)
when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name ->
VtSideff [], VtNow
- (* Nested vernac exprs *)
- | VernacProgram e -> static_classifier ~poly e
- | VernacLocal (_,e) -> static_classifier ~poly e
- | VernacPolymorphic (b, e) -> static_classifier ~poly:b e
(* Qed *)
| VernacAbort _ -> VtQed VtDrop, VtLater
| VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater
@@ -193,7 +189,13 @@ let classify_vernac e =
with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
in
let rec static_control_classifier ~poly = function
- | VernacExpr e -> static_classifier ~poly e
+ | VernacExpr (f, e) ->
+ let poly = List.fold_left (fun poly f ->
+ match f with
+ | VernacPolymorphic b -> b
+ | (VernacProgram | VernacLocal _) -> poly
+ ) poly f in
+ static_classifier ~poly e
| VernacTimeout (_,e) -> static_control_classifier ~poly e
| VernacTime (_,(_,e)) | VernacRedirect (_, (_,e)) ->
static_control_classifier ~poly e
diff --git a/test-suite/success/BracketsWithGoalSelector.v b/test-suite/success/BracketsWithGoalSelector.v
new file mode 100644
index 0000000000..ed035f5213
--- /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/tools/md5sum.ml b/tools/md5sum.ml
new file mode 100644
index 0000000000..2fdcacc839
--- /dev/null
+++ b/tools/md5sum.ml
@@ -0,0 +1,24 @@
+let get_content file =
+ let ic = open_in_bin file in
+ let buf = Buffer.create 2048 in
+ let rec fill () =
+ match input_char ic with
+ | '\r' -> fill () (* NOTE: handles the case on Windows where the
+ git checkout has included return characters.
+ See: https://github.com/coq/coq/pull/6305 *)
+ | c -> Buffer.add_char buf c; fill ()
+ | exception End_of_file -> close_in ic; Buffer.contents buf
+ in
+ fill ()
+
+let () =
+ match Sys.argv with
+ | [|_; file|] ->
+ let content = get_content file in
+ let md5 = Digest.to_hex (Digest.string content) in
+ print_string (md5 ^ " " ^ file)
+ | _ ->
+ prerr_endline "Error: This program needs exactly one parameter.";
+ prerr_endline "Usage: ocaml md5sum.ml <FILE>";
+ prerr_endline "Print MD5 (128-bit) checksum of the file content modulo \\r.";
+ exit 1
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ded0d97e64..3358951f4c 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 ->
@@ -1959,11 +1958,6 @@ let interp ?proof ~atts ~st c =
(* This one is possible to handle here *)
| VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command")
- (* Handled elsewhere *)
- | VernacProgram _
- | VernacPolymorphic _
- | VernacLocal _ -> assert false
-
(* Syntax *)
| VernacSyntaxExtension (infix, sl) ->
vernac_syntax_extension atts infix sl
@@ -2200,10 +2194,30 @@ let with_fail st b f =
let interp ?(verbosely=true) ?proof ~st (loc,c) =
let orig_univ_poly = Flags.is_universe_polymorphism () in
let orig_program_mode = Flags.is_program_mode () in
+ let flags f atts =
+ List.fold_left
+ (fun (polymorphism, atts) f ->
+ match f with
+ | VernacProgram when not atts.program ->
+ (polymorphism, { atts with program = true })
+ | VernacProgram ->
+ user_err Pp.(str "Program mode specified twice")
+ | VernacPolymorphic b when polymorphism = None ->
+ (Some b, atts)
+ | VernacPolymorphic _ ->
+ user_err Pp.(str "Polymorphism specified twice")
+ | VernacLocal b when Option.is_empty atts.locality ->
+ (polymorphism, { atts with locality = Some b })
+ | VernacLocal _ ->
+ user_err Pp.(str "Locality specified twice")
+ )
+ (None, atts)
+ f
+ in
let rec control = function
- | VernacExpr v ->
- let atts = { loc; locality = None; polymorphic = false; } in
- aux ~atts orig_program_mode v
+ | VernacExpr (f, v) ->
+ let (polymorphism, atts) = flags f { loc; locality = None; polymorphic = false; program = orig_program_mode; } in
+ aux ~polymorphism ~atts v
| VernacFail v -> with_fail st true (fun () -> control v)
| VernacTimeout (n,v) ->
current_timeout := Some n;
@@ -2213,25 +2227,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
| VernacTime (batch, (_loc,v)) ->
System.with_time ~batch control v;
- and aux ?polymorphism ~atts isprogcmd = function
-
- | VernacProgram c when not isprogcmd ->
- aux ?polymorphism ~atts true c
-
- | VernacProgram _ ->
- user_err Pp.(str "Program mode specified twice")
-
- | VernacPolymorphic (b, c) when polymorphism = None ->
- aux ~polymorphism:b ~atts:atts isprogcmd c
-
- | VernacPolymorphic (b, c) ->
- user_err Pp.(str "Polymorphism specified twice")
-
- | VernacLocal (b, c) when Option.is_empty atts.locality ->
- aux ?polymorphism ~atts:{atts with locality = Some b} isprogcmd c
-
- | VernacLocal _ ->
- user_err Pp.(str "Locality specified twice")
+ and aux ~polymorphism ~atts : _ -> unit =
+ function
| VernacLoad (_,fname) -> vernac_load control fname
@@ -2240,7 +2237,7 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
check_vernac_supports_polymorphism c polymorphism;
let polymorphic = Option.default (Flags.is_universe_polymorphism ()) polymorphism in
Flags.make_universe_polymorphism polymorphic;
- Obligations.set_program_mode isprogcmd;
+ Obligations.set_program_mode atts.program;
try
vernac_timeout begin fun () ->
let atts = { atts with polymorphic } in
@@ -2249,7 +2246,7 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
else Flags.silently (interp ?proof ~atts ~st) c;
(* If the command is `(Un)Set Program Mode` or `(Un)Set Universe Polymorphism`,
we should not restore the previous state of the flag... *)
- if orig_program_mode || not !Flags.program_mode || isprogcmd then
+ if orig_program_mode || not !Flags.program_mode || atts.program then
Flags.program_mode := orig_program_mode;
if (Flags.is_universe_polymorphism() = polymorphic) then
Flags.make_universe_polymorphism orig_univ_poly;
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index c0b93c1638..c40ca27dba 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -16,6 +16,7 @@ type atts = {
loc : Loc.t option;
locality : bool option;
polymorphic : bool;
+ program : bool;
}
type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index ab3d4bfc52..c5e610f89c 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -14,6 +14,7 @@ type atts = {
loc : Loc.t option;
locality : bool option;
polymorphic : bool;
+ program : bool;
}
type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 4fdc78dd2a..3932d1c7b5 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -12,14 +12,14 @@
open Vernacexpr
let rec under_control = function
- | VernacExpr c -> c
+ | VernacExpr (_, c) -> c
| VernacRedirect (_,(_,c))
| VernacTime (_,(_,c))
| VernacFail c
| VernacTimeout (_,c) -> under_control c
let rec has_Fail = function
- | VernacExpr c -> false
+ | VernacExpr _ -> false
| VernacRedirect (_,(_,c))
| VernacTime (_,(_,c))
| VernacTimeout (_,c) -> has_Fail c
@@ -45,8 +45,8 @@ let rec is_deep_navigation_vernac = function
(* NB: Reset is now allowed again as asked by A. Chlipala *)
let is_reset = function
- | VernacExpr VernacResetInitial
- | VernacExpr (VernacResetName _) -> true
+ | VernacExpr ( _, VernacResetInitial)
+ | VernacExpr (_, VernacResetName _) -> true
| _ -> false
let is_debug cmd = match under_control cmd with
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 22:56:32 +0000