Merge PR #9222: Fix classification of Set Default Proof Mode.

1 files changed, 2 insertions, 1 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 8077da8807..3214735ddf 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -53,11 +53,12 @@ let default_proof_mode = ref (find_proof_mode "No")
 let get_default_proof_mode_name () =
   (CEphemeron.default !default_proof_mode standard).name
 
+let proof_mode_opt_name = ["Default";"Proof";"Mode"]
 let () =
   Goptions.(declare_string_option {
     optdepr = false;
     optname = "default proof mode" ;
-    optkey = ["Default";"Proof";"Mode"] ;
+    optkey = proof_mode_opt_name ;
     optread = begin fun () ->
       (CEphemeron.default !default_proof_mode standard).name
     end;