Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"

The "Classic" string is still hard coded here in there in the system, but
not in STM.
BTW, the use of an hard coded "Classic" value suggests nobody really uses
"Set Default Proof Mode" in .v files.

1 files changed, 7 insertions, 3 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 647dbe111..36277bf58 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -23,8 +23,9 @@ open Names
 (* 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 : string ;
+  name : proof_mode_name ;
   set : unit -> unit ;
   reset : unit -> unit
 }
@@ -45,6 +46,9 @@ 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 _ =
   Goptions.declare_string_option {Goptions.
     optsync = true ;
@@ -219,8 +223,8 @@ let set_proof_mode mn =
 
 let activate_proof_mode mode =
   CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ())
-let disactivate_proof_mode mode =
-  CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.reset ())
+let disactivate_current_proof_mode () =
+  CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ())
 
 (** [start_proof sigma id str goals terminator] starts a proof of name
     [id] with goals [goals] (a list of pairs of environment and