diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 92 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 45 |
2 files changed, 6 insertions, 131 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 4cc73f419e..9ee9e7ae2c 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -22,51 +22,6 @@ open Names module NamedDecl = Context.Named.Declaration -(*** Proof Modes ***) - -(* Type of proof modes : - - A function [set] to set it *from standard mode* - - A function [reset] to reset the *standard mode* from it *) -type proof_mode_name = string -type proof_mode = { - name : proof_mode_name ; - set : unit -> unit ; - reset : unit -> unit -} - -let proof_modes = Hashtbl.create 6 -let find_proof_mode n = - try Hashtbl.find proof_modes n - with Not_found -> - CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." n)) - -let register_proof_mode ({name = n} as m) = - Hashtbl.add proof_modes n (CEphemeron.create m) - -(* initial mode: standard mode *) -let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) } -let _ = register_proof_mode standard - -(* Default proof mode, to be set at the beginning of proofs. *) -let default_proof_mode = ref (find_proof_mode "No") - -let get_default_proof_mode_name () = - (CEphemeron.default !default_proof_mode standard).name - -let proof_mode_opt_name = ["Default";"Proof";"Mode"] -let () = - Goptions.(declare_string_option { - optdepr = false; - optname = "default proof mode" ; - optkey = proof_mode_opt_name ; - optread = begin fun () -> - (CEphemeron.default !default_proof_mode standard).name - end; - optwrite = begin fun n -> - default_proof_mode := find_proof_mode n - end - }) - (*** Proof Global Environment ***) (* Extra info on proofs. *) @@ -95,7 +50,6 @@ type pstate = { endline_tactic : Genarg.glob_generic_argument option; section_vars : Constr.named_context option; proof : Proof.t; - mode : proof_mode CEphemeron.key; universe_decl: UState.universe_decl; strength : Decl_kinds.goal_kind; } @@ -109,23 +63,8 @@ let apply_terminator f = f to be resumed when the current proof is closed or aborted. *) let pstates = ref ([] : pstate list) -(* Current proof_mode, for bookkeeping *) -let current_proof_mode = ref !default_proof_mode - -(* combinators for proof modes *) -let update_proof_mode () = - match !pstates with - | { mode = m } :: _ -> - CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); - current_proof_mode := m; - CEphemeron.iter_opt !current_proof_mode (fun x -> x.set ()) - | _ -> - CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); - current_proof_mode := find_proof_mode "No" - (* combinators for the current_proof lists *) -let push a l = l := a::!l; - update_proof_mode () +let push a l = l := a::!l exception NoSuchProof let () = CErrors.register_handler begin function @@ -221,25 +160,8 @@ let discard {CAst.loc;v=id} = let discard_current () = if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates - let discard_all () = pstates := [] -(* [set_proof_mode] sets the proof mode to be used after it's called. It is - typically called by the Proof Mode command. *) -let set_proof_mode m id = - pstates := List.map - (fun ps -> if pf_name_eq id ps then { ps with mode = m } else ps) - !pstates; - update_proof_mode () - -let set_proof_mode mn = - set_proof_mode (find_proof_mode mn) (get_current_proof_name ()) - -let activate_proof_mode mode = - CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ()) -let disactivate_current_proof_mode () = - CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()) - (** [start_proof sigma id pl str goals terminator] starts a proof of name [id] with goals [goals] (a list of pairs of environment and conclusion); [str] describes what kind of theorem/definition this @@ -254,9 +176,8 @@ let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals terminator proof = Proof.start ~name ~poly:(pi2 kind) sigma goals; endline_tactic = None; section_vars = None; - mode = find_proof_mode "No"; - universe_decl = pl; - strength = kind } in + strength = kind; + universe_decl = pl } in push initial_state pstates let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator = @@ -265,9 +186,8 @@ let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals termina proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals; endline_tactic = None; section_vars = None; - mode = find_proof_mode "No"; - universe_decl = pl; - strength = kind } in + strength = kind; + universe_decl = pl } in push initial_state pstates let get_used_variables () = (cur_pstate ()).section_vars @@ -478,7 +398,7 @@ end let freeze ~marshallable = if marshallable then CErrors.anomaly (Pp.str"full marshalling of proof state not supported.") else !pstates -let unfreeze s = pstates := s; update_proof_mode () +let unfreeze s = pstates := s let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof let copy_terminators ~src ~tgt = assert(List.length src = List.length tgt); diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index e762f3b7dc..40920f51a3 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -13,7 +13,6 @@ environment. *) type t - val there_are_pending_proofs : unit -> bool val check_no_pending_proof : unit -> unit @@ -139,47 +138,3 @@ val freeze : marshallable:bool -> t val unfreeze : t -> unit val proof_of_state : t -> Proof.t val copy_terminators : src:t -> tgt:t -> t - - -(**********************************************************) -(* Proof Mode API *) -(* The current Proof Mode API is deprecated and a new one *) -(* will be (hopefully) defined in 8.8 *) -(**********************************************************) - -(** Type of proof modes : - - A name - - A function [set] to set it *from standard mode* - - A function [reset] to reset the *standard mode* from it - -*) -type proof_mode_name = string -type proof_mode = { - name : proof_mode_name ; - set : unit -> unit ; - reset : unit -> unit -} - -(** Registers a new proof mode which can then be adressed by name - in [set_default_proof_mode]. - One mode is already registered - the standard mode - named "No", - It corresponds to Coq default setting are they are set when coqtop starts. *) -val register_proof_mode : proof_mode -> unit -(* Can't make this deprecated due to limitations of camlp5 *) -(* [@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] *) - -val proof_mode_opt_name : string list - -val get_default_proof_mode_name : unit -> proof_mode_name -[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] - -(** [set_proof_mode] sets the proof mode to be used after it's called. It is - typically called by the Proof Mode command. *) -val set_proof_mode : proof_mode_name -> unit -[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] - -val activate_proof_mode : proof_mode_name -> unit -[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] - -val disactivate_current_proof_mode : unit -> unit -[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] |