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.

4 files changed, 27 insertions, 16 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
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index ebe7f6d6f..59daa2968 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -16,8 +16,9 @@
     - 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
 }
@@ -27,6 +28,7 @@ type 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,7 +42,7 @@ 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 : string -> unit
+val set_proof_mode : proof_mode_name -> unit
 
 exception NoCurrentProof
 val give_me_the_proof : unit -> Proof.proof
@@ -153,8 +155,8 @@ val get_universe_binders : unit -> universe_binders option
 (**********************************************************)
 
 
-val activate_proof_mode : string -> unit
-val disactivate_proof_mode : string -> unit
+val activate_proof_mode : proof_mode_name -> unit
+val disactivate_current_proof_mode : unit -> unit
 
 (**********************************************************)
 (*                                                        *)
diff --git a/stm/stm.ml b/stm/stm.ml
index f16b115e4..8f11875b6 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -83,6 +83,8 @@ let async_proofs_workers_extra_env = ref [||]
 type ast = { verbose : bool; loc : Loc.t; mutable expr : vernac_expr }
 let pr_ast { expr } = pr_vernac expr
 
+let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
+
 (* Commands piercing opaque *)
 let may_pierce_opaque = function
   | { expr = VernacPrint (PrintName _) } -> true
@@ -482,7 +484,7 @@ end = struct (* {{{ *)
         Proof_global.activate_proof_mode mode
       with Failure _ ->
         checkout Branch.master;
-        Proof_global.disactivate_proof_mode "Classic"
+        Proof_global.disactivate_current_proof_mode ()
 
   (* copies the transaction on every open branch *)
   let propagate_sideff ~replay:t =
@@ -2286,8 +2288,9 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
                 | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity
                 | _ -> Doesn'tGuaranteeOpacity in
               VCS.commit id (Fork (x,bname,opacity_of_produced_term,[]));
-              VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1));
-              Proof_global.activate_proof_mode "Classic";
+              let proof_mode = default_proof_mode () in
+              VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1));
+              Proof_global.activate_proof_mode proof_mode;
             end else begin
 	      VCS.commit id (Cmd {
                 ctac=false;ceff=in_proof;cast=x;cids=[];cqueue=`MainQueue });
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index ecaf0fb7c..b1df3c9ca 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -10,6 +10,8 @@ open Vernacexpr
 open Errors
 open Pp
 
+let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
+
 let string_of_in_script b = if b then " (inside script)" else ""
 
 let string_of_vernac_type = function
@@ -115,27 +117,27 @@ let rec classify_vernac e =
     (* StartProof *)
     | VernacDefinition (
        (Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) ->
-        VtStartProof("Classic",Doesn'tGuaranteeOpacity,[i]), VtLater
+        VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater
     | VernacDefinition (_,((_,i),_),ProveBody _) ->
-        VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater
+        VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater
     | VernacStartTheoremProof (_,l,_) ->
         let ids = 
           CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in
-        VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
-    | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater
+        VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
+    | VernacGoal _ -> VtStartProof (default_proof_mode (),GuaranteesOpacity,[]), VtLater
     | VernacFixpoint (_,l) ->
         let ids, open_proof =
           List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
         if open_proof
-        then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
+        then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
         else VtSideff ids, VtLater
     | VernacCoFixpoint (_,l) ->
         let ids, open_proof =
           List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
         if open_proof
-        then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
+        then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
         else VtSideff ids, VtLater
     (* Sideff: apply to all open branches. usually run on master only *)
     | VernacAssumption (_,_,l) ->