diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 40 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 9 |
2 files changed, 49 insertions, 0 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 5e11cfdb2d..2ca95d9584 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -410,6 +410,46 @@ module Bullet = struct end +(**********************************************************) +(* *) +(* 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 print_goal_selector = function + | Vernacexpr.SelectAll -> "all" + | Vernacexpr.SelectNth i -> string_of_int i + +let parse_goal_selector = function + | "all" -> Vernacexpr.SelectAll + | i -> + let err_msg = "A selector must be \"all\" or a natural number." in + begin try + let i = int_of_string i in + if i < 0 then Errors.error err_msg; + Vernacexpr.SelectNth i + with Failure _ -> Errors.error err_msg + end + +let _ = + Goptions.declare_string_option {Goptions. + optsync = true ; + optdepr = false; + optname = "default goal selector" ; + optkey = ["Default";"Goal";"Selector"] ; + optread = begin fun () -> print_goal_selector !default_goal_selector end; + optwrite = begin fun n -> + default_goal_selector := parse_goal_selector n + end + } + + module V82 = struct let get_current_initial_conclusions () = let { pid; strength; hook; proof } = cur_pstate () in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 867010fb05..b710b4ffe4 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -144,6 +144,15 @@ module Bullet : sig val put : Proof.proof -> t -> Proof.proof end + +(**********************************************************) +(* *) +(* Default goal selector *) +(* *) +(**********************************************************) + +val get_default_goal_selector : unit -> Vernacexpr.goal_selector + module V82 : sig val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list * Decl_kinds.goal_kind * unit Tacexpr.declaration_hook Ephemeron.key) |