aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/g_vernac.ml41
-rw-r--r--plugins/ltac/g_ltac.ml42
-rw-r--r--plugins/ltac/pptactic.mli2
-rw-r--r--plugins/ltac/tacexpr.ml4
-rw-r--r--plugins/ltac/tacexpr.mli4
-rw-r--r--pretyping/vernacexpr.ml27
-rw-r--r--printing/ppvernac.ml11
-rw-r--r--proofs/goal_select.ml68
-rw-r--r--proofs/goal_select.mli26
-rw-r--r--proofs/pfedit.ml14
-rw-r--r--proofs/pfedit.mli2
-rw-r--r--proofs/proof_bullet.ml70
-rw-r--r--proofs/proof_bullet.mli19
-rw-r--r--proofs/proof_global.ml1
-rw-r--r--proofs/proofs.mllib1
-rw-r--r--stm/proofBlockDelimiter.ml4
-rw-r--r--stm/proofBlockDelimiter.mli4
-rw-r--r--stm/stm.ml2
-rw-r--r--tactics/tacticals.ml12
-rw-r--r--tactics/tacticals.mli2
-rw-r--r--vernac/vernacentries.ml6
21 files changed, 163 insertions, 119 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 2dbd624c2..3026be248 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -48,6 +48,7 @@ let instance_name = Gram.entry_create "vernac:instance_name"
let section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
let make_bullet s =
+ let open Proof_bullet in
let n = String.length s in
match s.[0] with
| '-' -> Dash n
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index a1d7d9b1a..4857beffa 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -416,7 +416,7 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false
VERNAC tactic_mode EXTEND VernacSolve
| [ - ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
[ classify_as_proofstep ] -> [
- let g = Option.default (Proof_bullet.get_default_goal_selector ()) g in
+ let g = Option.default (Goal_select.get_default_goal_selector ()) g in
vernac_solve g n t def
]
| [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index aea00c240..799a52cc8 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -84,7 +84,7 @@ type pp_tactic = {
pptac_prods : grammar_terminals;
}
-val pr_goal_selector : toplevel:bool -> Vernacexpr.goal_selector -> Pp.t
+val pr_goal_selector : toplevel:bool -> Goal_select.t -> Pp.t
val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 37abfeee9..17f5e5d41 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -35,7 +35,7 @@ type advanced_flag = bool (* true = advanced false = basic *)
type letin_flag = bool (* true = use local def false = use Leibniz *)
type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
-type goal_selector = Vernacexpr.goal_selector =
+type goal_selector = Goal_select.t =
| SelectAlreadyFocused
| SelectNth of int
| SelectList of (int * int) list
@@ -270,7 +270,7 @@ and 'a gen_tactic_expr =
('p,'a gen_tactic_expr) match_rule list
| TacFun of 'a gen_tactic_fun_ast
| TacArg of 'a gen_tactic_arg located
- | TacSelect of Vernacexpr.goal_selector * 'a gen_tactic_expr
+ | TacSelect of Goal_select.t * 'a gen_tactic_expr
(* For ML extensions *)
| TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located
(* For syntax extensions *)
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 37abfeee9..17f5e5d41 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -35,7 +35,7 @@ type advanced_flag = bool (* true = advanced false = basic *)
type letin_flag = bool (* true = use local def false = use Leibniz *)
type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
-type goal_selector = Vernacexpr.goal_selector =
+type goal_selector = Goal_select.t =
| SelectAlreadyFocused
| SelectNth of int
| SelectList of (int * int) list
@@ -270,7 +270,7 @@ and 'a gen_tactic_expr =
('p,'a gen_tactic_expr) match_rule list
| TacFun of 'a gen_tactic_fun_ast
| TacArg of 'a gen_tactic_arg located
- | TacSelect of Vernacexpr.goal_selector * 'a gen_tactic_expr
+ | TacSelect of Goal_select.t * 'a gen_tactic_expr
(* For ML extensions *)
| TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located
(* For syntax extensions *)
diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml
index 548689205..8bf810498 100644
--- a/pretyping/vernacexpr.ml
+++ b/pretyping/vernacexpr.ml
@@ -16,17 +16,13 @@ open Libnames
(** Vernac expressions, produced by the parser *)
type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
-(* spiwack: I'm choosing, for now, to have [goal_selector] be a
- different type than [goal_reference] mostly because if it makes sense
- to print a goal that is out of focus (or already solved) it doesn't
- make sense to apply a tactic to it. Hence it the types may look very
- similar, they do not seem to mean the same thing. *)
-type goal_selector =
+type goal_selector = Goal_select.t =
| SelectAlreadyFocused
| SelectNth of int
| SelectList of (int * int) list
| SelectId of Id.t
| SelectAll
+[@@ocaml.deprecated "Use Goal_select.t"]
type goal_identifier = string
type scope_name = string
@@ -69,7 +65,7 @@ type printable =
| PrintScopes
| PrintScope of string
| PrintVisibility of string option
- | PrintAbout of reference or_by_notation * Universes.univ_name_list option * goal_selector option
+ | PrintAbout of reference or_by_notation * Universes.univ_name_list option * Goal_select.t option
| PrintImplicit of reference or_by_notation
| PrintAssumptions of bool * bool * reference or_by_notation
| PrintStrategy of reference or_by_notation option
@@ -198,7 +194,6 @@ type one_inductive_expr =
ident_decl * local_binder_expr list * constr_expr option * constructor_expr list
type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr
-
and typeclass_context = typeclass_constraint list
type proof_expr =
@@ -270,13 +265,11 @@ type extend_name =
(* This type allows registering the inlining of constants in native compiler.
It will be extended with primitive inductive types and operators *)
-type register_kind =
+type register_kind =
| RegisterInline
-type bullet =
- | Dash of int
- | Star of int
- | Plus of int
+type bullet = Proof_bullet.t
+[@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"]
(** {6 Types concerning the module layer} *)
@@ -426,11 +419,11 @@ type nonrec vernac_expr =
| VernacRemoveOption of Goptions.option_name * option_ref_value list
| VernacMemOption of Goptions.option_name * option_ref_value list
| VernacPrintOption of Goptions.option_name
- | VernacCheckMayEval of Genredexpr.raw_red_expr option * goal_selector option * constr_expr
+ | VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * constr_expr
| VernacGlobalCheck of constr_expr
| VernacDeclareReduction of string * Genredexpr.raw_red_expr
| VernacPrint of printable
- | VernacSearch of searchable * goal_selector option * search_restriction
+ | VernacSearch of searchable * Goal_select.t option * search_restriction
| VernacLocate of locatable
| VernacRegister of lident * register_kind
| VernacComments of comment list
@@ -444,8 +437,8 @@ type nonrec vernac_expr =
| VernacFocus of int option
| VernacUnfocus
| VernacUnfocused
- | VernacBullet of bullet
- | VernacSubproof of goal_selector option
+ | VernacBullet of Proof_bullet.t
+ | VernacSubproof of Goal_select.t option
| VernacEndSubproof
| VernacShow of showable
| VernacCheckGuard
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 83c875707..89117caf4 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -145,7 +145,7 @@ open Pputils
| SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
let pr_search a gopt b pr_p =
- pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt
+ pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt
++
match a with
| SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b
@@ -508,7 +508,7 @@ open Pputils
| PrintVisibility s ->
keyword "Print Visibility" ++ pr_opt str s
| PrintAbout (qid,l,gopt) ->
- pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt
+ pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt
++ keyword "About" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list l
| PrintImplicit qid ->
keyword "Print Implicit" ++ spc() ++ pr_smart_global qid
@@ -1122,7 +1122,7 @@ open Pputils
| None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c)
in
let pr_i = match io with None -> mt ()
- | Some i -> Proof_bullet.pr_goal_selector i ++ str ": " in
+ | Some i -> Goal_select.pr_goal_selector i ++ str ": " in
return (pr_i ++ pr_mayeval r c)
| VernacGlobalCheck c ->
return (hov 2 (keyword "Type" ++ pr_constrarg c))
@@ -1176,7 +1176,8 @@ open Pputils
| VernacProofMode s ->
return (keyword "Proof Mode" ++ str s)
| VernacBullet b ->
- return (begin match b with
+ (* XXX: Redundant with Proof_bullet.print *)
+ return (let open Proof_bullet in begin match b with
| Dash n -> str (String.make n '-')
| Star n -> str (String.make n '*')
| Plus n -> str (String.make n '+')
@@ -1184,7 +1185,7 @@ open Pputils
| VernacSubproof None ->
return (str "{")
| VernacSubproof (Some i) ->
- return (Proof_bullet.pr_goal_selector i ++ str ":" ++ spc () ++ str "{")
+ return (Goal_select.pr_goal_selector i ++ str ":" ++ spc () ++ str "{")
| VernacEndSubproof ->
return (str "}")
diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml
new file mode 100644
index 000000000..65a94a2c6
--- /dev/null
+++ b/proofs/goal_select.ml
@@ -0,0 +1,68 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+
+(* spiwack: I'm choosing, for now, to have [goal_selector] be a
+ different type than [goal_reference] mostly because if it makes sense
+ to print a goal that is out of focus (or already solved) it doesn't
+ make sense to apply a tactic to it. Hence it the types may look very
+ similar, they do not seem to mean the same thing. *)
+type t =
+ | SelectAlreadyFocused
+ | SelectNth of int
+ | SelectList of (int * int) list
+ | SelectId of Id.t
+ | SelectAll
+
+(* Default goal selector: selector chosen when a tactic is applied
+ without an explicit selector. *)
+let default_goal_selector = ref (SelectNth 1)
+let get_default_goal_selector () = !default_goal_selector
+
+let pr_range_selector (i, j) =
+ if i = j then Pp.int i
+ else Pp.(int i ++ str "-" ++ int j)
+
+let pr_goal_selector = function
+ | SelectAlreadyFocused -> Pp.str "!"
+ | SelectAll -> Pp.str "all"
+ | SelectNth i -> Pp.int i
+ | SelectList l ->
+ Pp.(str "["
+ ++ prlist_with_sep pr_comma pr_range_selector l
+ ++ str "]")
+ | SelectId id -> Names.Id.print id
+
+let parse_goal_selector = function
+ | "!" -> SelectAlreadyFocused
+ | "all" -> SelectAll
+ | i ->
+ let err_msg = "The default selector must be \"all\" or a natural number." in
+ begin try
+ let i = int_of_string i in
+ if i < 0 then CErrors.user_err Pp.(str err_msg);
+ SelectNth i
+ with Failure _ -> CErrors.user_err Pp.(str err_msg)
+ end
+
+let _ = let open Goptions in
+ declare_string_option
+ { optdepr = false;
+ optname = "default goal selector" ;
+ optkey = ["Default";"Goal";"Selector"] ;
+ optread = begin fun () ->
+ Pp.string_of_ppcmds
+ (pr_goal_selector !default_goal_selector)
+ end;
+ optwrite = begin fun n ->
+ default_goal_selector := parse_goal_selector n
+ end
+ }
diff --git a/proofs/goal_select.mli b/proofs/goal_select.mli
new file mode 100644
index 000000000..b1c572388
--- /dev/null
+++ b/proofs/goal_select.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+
+(* spiwack: I'm choosing, for now, to have [goal_selector] be a
+ different type than [goal_reference] mostly because if it makes sense
+ to print a goal that is out of focus (or already solved) it doesn't
+ make sense to apply a tactic to it. Hence it the types may look very
+ similar, they do not seem to mean the same thing. *)
+type t =
+ | SelectAlreadyFocused
+ | SelectNth of int
+ | SelectList of (int * int) list
+ | SelectId of Id.t
+ | SelectAll
+
+val pr_goal_selector : t -> Pp.t
+val get_default_goal_selector : unit -> t
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 62a38fa32..03c0969fa 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -100,8 +100,8 @@ let solve ?with_end_tac gi info_lvl tac pr =
| None -> tac
| Some _ -> Proofview.Trace.record_info_trace tac
in
- let tac = match gi with
- | Vernacexpr.SelectAlreadyFocused ->
+ let tac = let open Goal_select in match gi with
+ | SelectAlreadyFocused ->
let open Proofview.Notations in
Proofview.numgoals >>= fun n ->
if n == 1 then tac
@@ -113,10 +113,10 @@ let solve ?with_end_tac gi info_lvl tac pr =
in
Proofview.tclZERO e
- | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac
- | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l tac
- | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac
- | Vernacexpr.SelectAll -> tac
+ | SelectNth i -> Proofview.tclFOCUS i i tac
+ | SelectList l -> Proofview.tclFOCUSLIST l tac
+ | SelectId id -> Proofview.tclFOCUSID id tac
+ | SelectAll -> tac
in
let tac =
if use_unification_heuristics () then
@@ -133,7 +133,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
with
Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof")
-let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
+let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac)
let instantiate_nth_evar_com n com =
Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 65cde3a3a..805635dfa 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -75,7 +75,7 @@ val current_proof_statement :
tac] applies [tac] to all subgoals. *)
val solve : ?with_end_tac:unit Proofview.tactic ->
- Vernacexpr.goal_selector -> int option -> unit Proofview.tactic ->
+ Goal_select.t -> int option -> unit Proofview.tactic ->
Proof.t -> Proof.t * bool
(** [by tac] applies tactic [tac] to the 1st subgoal of the current
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index d6f7c0e93..cc3e79f85 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -10,19 +10,22 @@
open Proof
-type t = Vernacexpr.bullet
+type t =
+ | Dash of int
+ | Star of int
+ | Plus of int
let bullet_eq b1 b2 = match b1, b2 with
-| Vernacexpr.Dash n1, Vernacexpr.Dash n2 -> n1 = n2
-| Vernacexpr.Star n1, Vernacexpr.Star n2 -> n1 = n2
-| Vernacexpr.Plus n1, Vernacexpr.Plus n2 -> n1 = n2
+| Dash n1, Dash n2 -> n1 = n2
+| Star n1, Star n2 -> n1 = n2
+| Plus n1, Plus n2 -> n1 = n2
| _ -> false
let pr_bullet b =
match b with
- | Vernacexpr.Dash n -> Pp.(str (String.make n '-'))
- | Vernacexpr.Star n -> Pp.(str (String.make n '*'))
- | Vernacexpr.Plus n -> Pp.(str (String.make n '+'))
+ | Dash n -> Pp.(str (String.make n '-'))
+ | Star n -> Pp.(str (String.make n '*'))
+ | Plus n -> Pp.(str (String.make n '+'))
type behavior = {
@@ -195,54 +198,5 @@ let put p b =
let suggest p =
(!current_behavior).suggest p
-(**********************************************************)
-(* *)
-(* Default goal selector *)
-(* *)
-(**********************************************************)
-
-
-(* Default goal selector: selector chosen when a tactic is applied
- without an explicit selector. *)
-let default_goal_selector = ref (Vernacexpr.SelectNth 1)
-let get_default_goal_selector () = !default_goal_selector
-
-let pr_range_selector (i, j) =
- if i = j then Pp.int i
- else Pp.(int i ++ str "-" ++ int j)
-
-let pr_goal_selector = function
- | Vernacexpr.SelectAlreadyFocused -> Pp.str "!"
- | Vernacexpr.SelectAll -> Pp.str "all"
- | Vernacexpr.SelectNth i -> Pp.int i
- | Vernacexpr.SelectList l ->
- Pp.(str "["
- ++ prlist_with_sep pr_comma pr_range_selector l
- ++ str "]")
- | Vernacexpr.SelectId id -> Names.Id.print id
-
-let parse_goal_selector = function
- | "!" -> Vernacexpr.SelectAlreadyFocused
- | "all" -> Vernacexpr.SelectAll
- | i ->
- let err_msg = "The default selector must be \"all\" or \"!\" or a natural number." in
- begin try
- let i = int_of_string i in
- if i < 0 then CErrors.user_err Pp.(str err_msg);
- Vernacexpr.SelectNth i
- with Failure _ -> CErrors.user_err Pp.(str err_msg)
- end
-
-let _ =
- Goptions.(declare_string_option{optdepr = false;
- optname = "default goal selector" ;
- optkey = ["Default";"Goal";"Selector"] ;
- optread = begin fun () ->
- Pp.string_of_ppcmds
- (pr_goal_selector !default_goal_selector)
- end;
- optwrite = begin fun n ->
- default_goal_selector := parse_goal_selector n
- end
- })
-
+let pr_goal_selector = Goal_select.pr_goal_selector
+let get_default_goal_selector = Goal_select.get_default_goal_selector
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
index ffbaa0fac..a09a7ec1d 100644
--- a/proofs/proof_bullet.mli
+++ b/proofs/proof_bullet.mli
@@ -14,7 +14,10 @@
(* *)
(**********************************************************)
-type t = Vernacexpr.bullet
+type t =
+ | Dash of int
+ | Star of int
+ | Plus of int
(** A [behavior] is the data of a put function which
is called when a bullet prefixes a tactic, a suggest function
@@ -42,12 +45,8 @@ val register_behavior : behavior -> unit
val put : Proof.t -> t -> Proof.t
val suggest : Proof.t -> Pp.t
-(**********************************************************)
-(* *)
-(* Default goal selector *)
-(* *)
-(**********************************************************)
-
-val pr_goal_selector : Vernacexpr.goal_selector -> Pp.t
-val get_default_goal_selector : unit -> Vernacexpr.goal_selector
-
+(** Deprecated *)
+val pr_goal_selector : Goal_select.t -> Pp.t
+[@@ocaml.deprecated "Please use [Goal_select.pr_goal_selector]"]
+val get_default_goal_selector : unit -> Goal_select.t
+[@@ocaml.deprecated "Please use [Goal_select.get_default_goal_selector]"]
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index fc7c437e6..842003bc8 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -83,6 +83,7 @@ type proof_ending =
| Proved of Vernacexpr.opacity_flag *
Misctypes.lident option *
proof_object
+
type proof_terminator = proof_ending -> unit
type closed_proof = proof_object * proof_terminator
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 058e839b4..197f71ca9 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -5,6 +5,7 @@ Proof_type
Logic
Refine
Proof
+Goal_select
Proof_bullet
Proof_global
Redexpr
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 0af766219..b8af2bcd5 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -23,8 +23,8 @@ val crawl :
static_block_declaration option
val unit_val : Stm.DynBlockData.t
-val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
-val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
+val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t
+val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t
val of_vernac_control_val : Vernacexpr.vernac_control -> Stm.DynBlockData.t
val to_vernac_control_val : Stm.DynBlockData.t -> Vernacexpr.vernac_control
diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli
index 9784de114..eacd3687a 100644
--- a/stm/proofBlockDelimiter.mli
+++ b/stm/proofBlockDelimiter.mli
@@ -38,6 +38,6 @@ val crawl :
val unit_val : Stm.DynBlockData.t
(* Bullets *)
-val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
-val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
+val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t
+val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t
diff --git a/stm/stm.ml b/stm/stm.ml
index cbd324f5c..9ea6a305e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2288,7 +2288,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
Proof_global.unfreeze proof;
Proof_global.with_current_proof (fun _ p ->
feedback ~id:id Feedback.AddedAxiom;
- fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ());
+ fst (Pfedit.solve Goal_select.SelectAll None tac p), ());
(* STATE SPEC:
* - start: Modifies the input state adding a proof.
* - end : maybe after recovery command.
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 82b178388..6c7db26c7 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -492,12 +492,12 @@ module New = struct
Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t)
(* Select a subset of the goals *)
- let tclSELECT = function
- | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i
- | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l
- | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id
- | Vernacexpr.SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here")
- | Vernacexpr.SelectAlreadyFocused ->
+ let tclSELECT = let open Goal_select in function
+ | SelectNth i -> Proofview.tclFOCUS i i
+ | SelectList l -> Proofview.tclFOCUSLIST l
+ | SelectId id -> Proofview.tclFOCUSID id
+ | SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here")
+ | SelectAlreadyFocused ->
anomaly ~label:"tclSELECT" Pp.(str "SelectAlreadyFocused not allowed here")
(* Check that holes in arguments have been resolved *)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 340d8fbf3..bc2f60186 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -223,7 +223,7 @@ module New : sig
val tclCOMPLETE : 'a tactic -> 'a tactic
val tclSOLVE : unit tactic list -> unit tactic
val tclPROGRESS : unit tactic -> unit tactic
- val tclSELECT : Vernacexpr.goal_selector -> 'a tactic -> 'a tactic
+ val tclSELECT : Goal_select.t -> 'a tactic -> 'a tactic
val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic
val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 564c0965b..f0e41d27c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -909,7 +909,7 @@ let vernac_set_used_variables e =
if List.is_empty to_clear then (p, ())
else
let tac = Tactics.clear to_clear in
- fst (Pfedit.solve SelectAll None tac p), ()
+ fst (Pfedit.solve Goal_select.SelectAll None tac p), ()
end
(*****************************)
@@ -1611,7 +1611,7 @@ let get_current_context_of_args = function
let query_command_selector ?loc = function
| None -> None
- | Some (SelectNth n) -> Some n
+ | Some (Goal_select.SelectNth n) -> Some n
| _ -> user_err ?loc ~hdr:"query_command_selector"
(str "Query commands only support the single numbered goal selector.")
@@ -1911,7 +1911,7 @@ let vernac_subproof gln =
Proof_global.simple_with_current_proof (fun _ p ->
match gln with
| None -> Proof.focus subproof_cond () 1 p
- | Some (SelectNth n) -> Proof.focus subproof_cond () n p
+ | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p
| _ -> user_err ~hdr:"bracket_selector"
(str "Brackets only support the single numbered goal selector."))
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 12:28:17 +0000