[proof] Deprecate "proof mode" API

Any users of this API should coordinate with the ongoing work in PRs
numbered #459 and #566.

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 "]
+