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.

2 files changed, 14 insertions, 9 deletions

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) ->