2 files changed, 13 insertions, 7 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 647dbe1115..36277bf58d 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 ebe7f6d6f3..59daa29681 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
 
 (**********************************************************)
 (*                                                        *)