aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-12 17:12:51 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-12 17:27:53 +0200
commitab53757a3bf57ced503023f3cf9dea5b5503dfea (patch)
tree97241209c0348d72fda82fa33d67095f39d32da3 /proofs
parent79c42e22dd5106dcb85229ceec75331029ab5486 (diff)
[proof] Move bullets to their own module.
Bullets were placed inside the `Proof_global` module, I guess that due to the global registration function. However, it has logically nothing to do with the functionality of `Proof_global` and the current placement may create some interference between the developers reworking proof state handling and bullets. We thus put the bullet functionality into its own, independent file.
Diffstat (limited to 'proofs')
-rw-r--r--proofs/proof_bullet.ml248
-rw-r--r--proofs/proof_bullet.mli53
-rw-r--r--proofs/proof_global.ml267
-rw-r--r--proofs/proof_global.mli46
-rw-r--r--proofs/proofs.mllib1
5 files changed, 310 insertions, 305 deletions
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
new file mode 100644
index 000000000..f80cb7cc6
--- /dev/null
+++ b/proofs/proof_bullet.ml
@@ -0,0 +1,248 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Proof
+
+type t = Vernacexpr.bullet
+
+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
+| _ -> 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 '+'))
+
+
+type behavior = {
+ name : string;
+ put : proof -> t -> proof;
+ suggest: proof -> Pp.t
+}
+
+let behaviors = Hashtbl.create 4
+let register_behavior b = Hashtbl.add behaviors b.name b
+
+(*** initial modes ***)
+let none = {
+ name = "None";
+ put = (fun x _ -> x);
+ suggest = (fun _ -> Pp.mt ())
+}
+let _ = register_behavior none
+
+module Strict = struct
+ type suggestion =
+ | Suggest of t (* this bullet is mandatory here *)
+ | Unfinished of t (* no mandatory bullet here, but this bullet is unfinished *)
+ | NoBulletInUse (* No mandatory bullet (or brace) here, no bullet pending,
+ some focused goals exists. *)
+ | NeedClosingBrace (* Some unfocussed goal exists "{" needed to focus them *)
+ | ProofFinished (* No more goal anywhere *)
+
+ (* give a message only if more informative than the standard coq message *)
+ let suggest_on_solved_goal sugg =
+ match sugg with
+ | NeedClosingBrace -> Pp.(str"Try unfocusing with \"}\".")
+ | NoBulletInUse -> Pp.mt ()
+ | ProofFinished -> Pp.mt ()
+ | Suggest b -> Pp.(str"Focus next goal with bullet " ++ pr_bullet b ++ str".")
+ | Unfinished b -> Pp.(str"The current bullet " ++ pr_bullet b ++ str" is unfinished.")
+
+ (* give always a message. *)
+ let suggest_on_error sugg =
+ match sugg with
+ | NeedClosingBrace -> Pp.(str"Try unfocusing with \"}\".")
+ | NoBulletInUse -> assert false (* This should never raise an error. *)
+ | ProofFinished -> Pp.(str"No more subgoals.")
+ | Suggest b -> Pp.(str"Expecting " ++ pr_bullet b ++ str".")
+ | Unfinished b -> Pp.(str"Current bullet " ++ pr_bullet b ++ str" is not finished.")
+
+ exception FailedBullet of t * suggestion
+
+ let _ =
+ CErrors.register_handler
+ (function
+ | FailedBullet (b,sugg) ->
+ let prefix = Pp.(str"Wrong bullet " ++ pr_bullet b ++ str": ") in
+ CErrors.user_err ~hdr:"Focus" Pp.(prefix ++ suggest_on_error sugg)
+ | _ -> raise CErrors.Unhandled)
+
+
+ (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *)
+ let bullet_kind = (new_focus_kind () : t list focus_kind)
+ let bullet_cond = done_cond ~loose_end:true bullet_kind
+
+ (* spiwack: as it is bullets are reset (locally) by *any* non-bullet focusing command
+ experience will tell if this is the right discipline of if we want to be finer and
+ reset them only for a choice of bullets. *)
+ let get_bullets pr =
+ if is_last_focus bullet_kind pr then
+ get_at_focus bullet_kind pr
+ else
+ []
+
+ let has_bullet bul pr =
+ let rec has_bullet = function
+ | b'::_ when bullet_eq bul b' -> true
+ | _::l -> has_bullet l
+ | [] -> false
+ in
+ has_bullet (get_bullets pr)
+
+ (* pop a bullet from proof [pr]. There should be at least one
+ bullet in use. If pop impossible (pending proofs on this level
+ of bullet or higher) then raise [Proof.CannotUnfocusThisWay]. *)
+ let pop pr =
+ match get_bullets pr with
+ | b::_ -> unfocus bullet_kind pr () , b
+ | _ -> assert false
+
+ let push (b:t) pr =
+ focus bullet_cond (b::get_bullets pr) 1 pr
+
+ (* Used only in the next function.
+ TODO: use a recursive function instead? *)
+ exception SuggestFound of t
+
+ let suggest_bullet (prf : proof): suggestion =
+ if is_done prf then ProofFinished
+ else if not (no_focused_goal prf)
+ then (* No suggestion if a bullet is not mandatory, look for an unfinished bullet *)
+ match get_bullets prf with
+ | b::_ -> Unfinished b
+ | _ -> NoBulletInUse
+ else (* There is no goal under focus but some are unfocussed,
+ let us look at the bullet needed. If no *)
+ let pcobaye = ref prf in
+ try
+ while true do
+ let pcobaye', b = pop !pcobaye in
+ (* pop went well, this means that there are no more goals
+ *under this* bullet b, see if a new b can be pushed. *)
+ (try let _ = push b pcobaye' in (* push didn't fail so a new b can be pushed. *)
+ raise (SuggestFound b)
+ with SuggestFound _ as e -> raise e
+ | _ -> ()); (* b could not be pushed, so we must look for a outer bullet *)
+ pcobaye := pcobaye'
+ done;
+ assert false
+ with SuggestFound b -> Suggest b
+ | _ -> NeedClosingBrace (* No push was possible, but there are still
+ subgoals somewhere: there must be a "}" to use. *)
+
+
+ let rec pop_until (prf : proof) bul : proof =
+ let prf', b = pop prf in
+ if bullet_eq bul b then prf'
+ else pop_until prf' bul
+
+ let put p bul =
+ try
+ if not (has_bullet bul p) then
+ (* bullet is not in use, so pushing it is always ok unless
+ no goal under focus. *)
+ push bul p
+ else
+ match suggest_bullet p with
+ | Suggest suggested_bullet when bullet_eq bul suggested_bullet
+ -> (* suggested_bullet is mandatory and you gave the right one *)
+ let p' = pop_until p bul in
+ push bul p'
+ (* the bullet you gave is in use but not the right one *)
+ | sugg -> raise (FailedBullet (bul,sugg))
+ with NoSuchGoals _ -> (* push went bad *)
+ raise (FailedBullet (bul,suggest_bullet p))
+
+ let strict = {
+ name = "Strict Subproofs";
+ put = put;
+ suggest = (fun prf -> suggest_on_solved_goal (suggest_bullet prf))
+
+ }
+ let _ = register_behavior strict
+end
+
+(* Current bullet behavior, controlled by the option *)
+let current_behavior = ref Strict.strict
+
+let _ =
+ Goptions.(declare_string_option {
+ optdepr = false;
+ optname = "bullet behavior";
+ optkey = ["Bullet";"Behavior"];
+ optread = begin fun () ->
+ (!current_behavior).name
+ end;
+ optwrite = begin fun n ->
+ current_behavior :=
+ try Hashtbl.find behaviors n
+ with Not_found ->
+ CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\"."))
+ end
+ })
+
+let put p b =
+ (!current_behavior).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.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
+ | "all" -> Vernacexpr.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);
+ 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
+ })
+
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
new file mode 100644
index 000000000..9ae521d3f
--- /dev/null
+++ b/proofs/proof_bullet.mli
@@ -0,0 +1,53 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(**********************************************************)
+(* *)
+(* Bullets *)
+(* *)
+(**********************************************************)
+
+open Proof
+
+type t = Vernacexpr.bullet
+
+(** A [behavior] is the data of a put function which
+ is called when a bullet prefixes a tactic, a suggest function
+ suggesting the right bullet to use on a given proof, together
+ with a name to identify the behavior. *)
+type behavior = {
+ name : string;
+ put : proof -> t -> proof;
+ suggest: proof -> Pp.t
+}
+
+(** A registered behavior can then be accessed in Coq
+ through the command [Set Bullet Behavior "name"].
+
+ Two modes are registered originally:
+ * "Strict Subproofs":
+ - If this bullet follows another one of its kind, defocuses then focuses
+ (which fails if the focused subproof is not complete).
+ - If it is the first bullet of its kind, then focuses a new subproof.
+ * "None": bullets don't do anything *)
+val register_behavior : behavior -> unit
+
+(** Handles focusing/defocusing with bullets:
+ *)
+val put : proof -> t -> proof
+val suggest : proof -> Pp.t
+
+(**********************************************************)
+(* *)
+(* Default goal selector *)
+(* *)
+(**********************************************************)
+
+val pr_goal_selector : Vernacexpr.goal_selector -> Pp.std_ppcmds
+val get_default_goal_selector : unit -> Vernacexpr.goal_selector
+
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 5ec34a638..d8d3a9027 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -447,265 +447,6 @@ let set_terminator hook =
| [] -> raise NoCurrentProof
| p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps
-
-
-
-(**********************************************************)
-(* *)
-(* Bullets *)
-(* *)
-(**********************************************************)
-
-module Bullet = struct
-
- type t = Vernacexpr.bullet
-
- 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
- | _ -> false
-
- let pr_bullet b =
- match b with
- | Vernacexpr.Dash n -> str (String.make n '-')
- | Vernacexpr.Star n -> str (String.make n '*')
- | Vernacexpr.Plus n -> str (String.make n '+')
-
-
- type behavior = {
- name : string;
- put : Proof.proof -> t -> Proof.proof;
- suggest: Proof.proof -> std_ppcmds
- }
-
- let behaviors = Hashtbl.create 4
- let register_behavior b = Hashtbl.add behaviors b.name b
-
- (*** initial modes ***)
- let none = {
- name = "None";
- put = (fun x _ -> x);
- suggest = (fun _ -> mt ())
- }
- let _ = register_behavior none
-
- module Strict = struct
- type suggestion =
- | Suggest of t (* this bullet is mandatory here *)
- | Unfinished of t (* no mandatory bullet here, but this bullet is unfinished *)
- | NoBulletInUse (* No mandatory bullet (or brace) here, no bullet pending,
- some focused goals exists. *)
- | NeedClosingBrace (* Some unfocussed goal exists "{" needed to focus them *)
- | ProofFinished (* No more goal anywhere *)
-
- (* give a message only if more informative than the standard coq message *)
- let suggest_on_solved_goal sugg =
- match sugg with
- | NeedClosingBrace -> str"Try unfocusing with \"}\"."
- | NoBulletInUse -> mt ()
- | ProofFinished -> mt ()
- | Suggest b -> str"Focus next goal with bullet " ++ pr_bullet b ++ str"."
- | Unfinished b -> str"The current bullet " ++ pr_bullet b ++ str" is unfinished."
-
- (* give always a message. *)
- let suggest_on_error sugg =
- match sugg with
- | NeedClosingBrace -> str"Try unfocusing with \"}\"."
- | NoBulletInUse -> assert false (* This should never raise an error. *)
- | ProofFinished -> str"No more subgoals."
- | Suggest b -> str"Expecting " ++ pr_bullet b ++ str"."
- | Unfinished b -> str"Current bullet " ++ pr_bullet b ++ str" is not finished."
-
- exception FailedBullet of t * suggestion
-
- let _ =
- CErrors.register_handler
- (function
- | FailedBullet (b,sugg) ->
- let prefix = str"Wrong bullet " ++ pr_bullet b ++ str": " in
- CErrors.user_err ~hdr:"Focus" (prefix ++ suggest_on_error sugg)
- | _ -> raise CErrors.Unhandled)
-
-
- (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *)
- let bullet_kind = (Proof.new_focus_kind () : t list Proof.focus_kind)
- let bullet_cond = Proof.done_cond ~loose_end:true bullet_kind
-
- (* spiwack: as it is bullets are reset (locally) by *any* non-bullet focusing command
- experience will tell if this is the right discipline of if we want to be finer and
- reset them only for a choice of bullets. *)
- let get_bullets pr =
- if Proof.is_last_focus bullet_kind pr then
- Proof.get_at_focus bullet_kind pr
- else
- []
-
- let has_bullet bul pr =
- let rec has_bullet = function
- | b'::_ when bullet_eq bul b' -> true
- | _::l -> has_bullet l
- | [] -> false
- in
- has_bullet (get_bullets pr)
-
- (* pop a bullet from proof [pr]. There should be at least one
- bullet in use. If pop impossible (pending proofs on this level
- of bullet or higher) then raise [Proof.CannotUnfocusThisWay]. *)
- let pop pr =
- match get_bullets pr with
- | b::_ -> Proof.unfocus bullet_kind pr () , b
- | _ -> assert false
-
- let push (b:t) pr =
- Proof.focus bullet_cond (b::get_bullets pr) 1 pr
-
- (* Used only in the next function.
- TODO: use a recursive function instead? *)
- exception SuggestFound of t
-
- let suggest_bullet (prf:Proof.proof): suggestion =
- if Proof.is_done prf then ProofFinished
- else if not (Proof.no_focused_goal prf)
- then (* No suggestion if a bullet is not mandatory, look for an unfinished bullet *)
- match get_bullets prf with
- | b::_ -> Unfinished b
- | _ -> NoBulletInUse
- else (* There is no goal under focus but some are unfocussed,
- let us look at the bullet needed. If no *)
- let pcobaye = ref prf in
- try
- while true do
- let pcobaye', b = pop !pcobaye in
- (* pop went well, this means that there are no more goals
- *under this* bullet b, see if a new b can be pushed. *)
- (try let _ = push b pcobaye' in (* push didn't fail so a new b can be pushed. *)
- raise (SuggestFound b)
- with SuggestFound _ as e -> raise e
- | _ -> ()); (* b could not be pushed, so we must look for a outer bullet *)
- pcobaye := pcobaye'
- done;
- assert false
- with SuggestFound b -> Suggest b
- | _ -> NeedClosingBrace (* No push was possible, but there are still
- subgoals somewhere: there must be a "}" to use. *)
-
-
- let rec pop_until (prf:Proof.proof) bul: Proof.proof =
- let prf', b = pop prf in
- if bullet_eq bul b then prf'
- else pop_until prf' bul
-
- let put p bul =
- try
- if not (has_bullet bul p) then
- (* bullet is not in use, so pushing it is always ok unless
- no goal under focus. *)
- push bul p
- else
- match suggest_bullet p with
- | Suggest suggested_bullet when bullet_eq bul suggested_bullet
- -> (* suggested_bullet is mandatory and you gave the right one *)
- let p' = pop_until p bul in
- push bul p'
- (* the bullet you gave is in use but not the right one *)
- | sugg -> raise (FailedBullet (bul,sugg))
- with Proof.NoSuchGoals _ -> (* push went bad *)
- raise (FailedBullet (bul,suggest_bullet p))
-
- let strict = {
- name = "Strict Subproofs";
- put = put;
- suggest = (fun prf -> suggest_on_solved_goal (suggest_bullet prf))
-
- }
- let _ = register_behavior strict
- end
-
- (* Current bullet behavior, controlled by the option *)
- let current_behavior = ref Strict.strict
-
- let _ =
- Goptions.(declare_string_option {
- optdepr = false;
- optname = "bullet behavior";
- optkey = ["Bullet";"Behavior"];
- optread = begin fun () ->
- (!current_behavior).name
- end;
- optwrite = begin fun n ->
- current_behavior :=
- try Hashtbl.find behaviors n
- with Not_found ->
- CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\"."))
- end
- })
-
- let put p b =
- (!current_behavior).put p b
-
- let suggest p =
- (!current_behavior).suggest p
-end
-
-
-let _ =
- let hook n =
- let prf = give_me_the_proof () in
- (Bullet.suggest prf) in
- Proofview.set_nosuchgoals_hook hook
-
-
-(**********************************************************)
-(* *)
-(* 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 int i
- else int i ++ str "-" ++ int j
-
-let pr_goal_selector = function
- | Vernacexpr.SelectAll -> str "all"
- | Vernacexpr.SelectNth i -> int i
- | Vernacexpr.SelectList l ->
- str "["
- ++ prlist_with_sep pr_comma pr_range_selector l
- ++ str "]"
- | Vernacexpr.SelectId id -> Id.print id
-
-let parse_goal_selector = function
- | "all" -> Vernacexpr.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);
- 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 () ->
- string_of_ppcmds
- (pr_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; proof } = cur_pstate () in
@@ -734,3 +475,11 @@ let update_global_env () =
let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac p in
(p, ())))
+
+(* XXX: Bullet hook, should be really moved elsewhere *)
+let _ =
+ let hook n =
+ let prf = give_me_the_proof () in
+ (Proof_bullet.suggest prf) in
+ Proofview.set_nosuchgoals_hook hook
+
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 22cc8cf59..bb9d66b6e 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -121,52 +121,6 @@ val get_used_variables : unit -> Context.Named.t option
val get_universe_binders : unit -> universe_binders option
-(**********************************************************)
-(* *)
-(* Bullets *)
-(* *)
-(**********************************************************)
-
-module Bullet : sig
- type t = Vernacexpr.bullet
-
- (** A [behavior] is the data of a put function which
- is called when a bullet prefixes a tactic, a suggest function
- suggesting the right bullet to use on a given proof, together
- with a name to identify the behavior. *)
- type behavior = {
- name : string;
- put : Proof.proof -> t -> Proof.proof;
- suggest: Proof.proof -> Pp.std_ppcmds
- }
-
- (** A registered behavior can then be accessed in Coq
- through the command [Set Bullet Behavior "name"].
-
- Two modes are registered originally:
- * "Strict Subproofs":
- - If this bullet follows another one of its kind, defocuses then focuses
- (which fails if the focused subproof is not complete).
- - If it is the first bullet of its kind, then focuses a new subproof.
- * "None": bullets don't do anything *)
- val register_behavior : behavior -> unit
-
- (** Handles focusing/defocusing with bullets:
- *)
- val put : Proof.proof -> t -> Proof.proof
- val suggest : Proof.proof -> Pp.std_ppcmds
-end
-
-
-(**********************************************************)
-(* *)
-(* Default goal selector *)
-(* *)
-(**********************************************************)
-
-val pr_goal_selector : Vernacexpr.goal_selector -> Pp.std_ppcmds
-val get_default_goal_selector : unit -> Vernacexpr.goal_selector
-
module V82 : sig
val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list *
Decl_kinds.goal_kind)
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 804a54360..0ea2bd66b 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -5,6 +5,7 @@ Proof_using
Logic
Refine
Proof
+Proof_bullet
Proof_global
Redexpr
Refiner