diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-06-07 11:23:41 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-07 11:23:41 +0200 |
commit | 77e4a3712dff87e5941dd93ebfa8028039ab0715 (patch) | |
tree | ca9db76e334d40fb19938b014a20c3691866092a /proofs | |
parent | 3e29266b1e2dfb970ca77fb5910b6a5860d4ad1a (diff) | |
parent | 48476a32fa9221b216074695cceeaa0b34fc659b (diff) |
Merge PR#717: [proof] Deprecate "proof mode" API
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/proof_global.mli | 77 |
1 files changed, 43 insertions, 34 deletions
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 52bbd9ac5..22cc8cf59 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -10,26 +10,6 @@ toplevel. In particular it defines the global proof environment. *) -(** 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 -val get_default_proof_mode_name : unit -> proof_mode_name - val there_are_pending_proofs : unit -> bool val check_no_pending_proof : unit -> unit @@ -40,10 +20,6 @@ val discard : Names.Id.t Loc.located -> unit val discard_current : unit -> unit val discard_all : unit -> unit -(** [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 - exception NoCurrentProof val give_me_the_proof : unit -> Proof.proof (** @raise NoCurrentProof when outside proof mode. *) @@ -147,16 +123,6 @@ val get_universe_binders : unit -> universe_binders option (**********************************************************) (* *) -(* Proof modes *) -(* *) -(**********************************************************) - - -val activate_proof_mode : proof_mode_name -> unit -val disactivate_current_proof_mode : unit -> unit - -(**********************************************************) -(* *) (* Bullets *) (* *) (**********************************************************) @@ -211,3 +177,46 @@ val freeze : marshallable:[`Yes | `No | `Shallow] -> state val unfreeze : state -> unit val proof_of_state : state -> Proof.proof val copy_terminators : src:state -> tgt:state -> state + + +(**********************************************************) +(* 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 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 "] + |