Fix coq/ltac2#15: Ltac2 scope cannot be disabled after it is required.

Instead of setting globally the option, we add a hook to set it in
the init object of the plugin.

2 files changed, 14 insertions, 8 deletions

diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index efdc995a69..a503a0ab4c 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -827,13 +827,21 @@ let t_list = coq_def "list"
 
 let (f_register_constr_quotations, register_constr_quotations) = Hook.make ()
 
-let perform_constr_quotations (_, ()) = Hook.get f_register_constr_quotations ()
+let cache_ltac2_init (_, ()) =
+  Hook.get f_register_constr_quotations ()
+
+let load_ltac2_init _ (_, ()) =
+  Hook.get f_register_constr_quotations ()
+
+let open_ltac2_init _ (_, ()) =
+  Goptions.set_string_option_value_gen None ["Default"; "Proof"; "Mode"] "Ltac2"
 
 (** Dummy object that register global rules when Require is called *)
-let inTac2ConstrQuotations : unit -> obj =
-  declare_object {(default_object "TAC2-CONSTR-QUOT") with
-    cache_function = perform_constr_quotations;
-    load_function = fun _ -> perform_constr_quotations;
+let inTac2Init : unit -> obj =
+  declare_object {(default_object "TAC2-INIT") with
+    cache_function = cache_ltac2_init;
+    load_function = load_ltac2_init;
+    open_function = open_ltac2_init;
   }
 
 let _ = Mltop.declare_cache_obj begin fun () ->
@@ -842,5 +850,5 @@ let _ = Mltop.declare_cache_obj begin fun () ->
     ("[]", []);
     ("::", [GTypVar 0; GTypRef (Other t_list, [GTypVar 0])]);
   ];
-  Lib.add_anonymous_leaf (inTac2ConstrQuotations ());
+  Lib.add_anonymous_leaf (inTac2Init ());
 end "ltac2_plugin"
diff --git a/theories/Init.v b/theories/Init.v
index 04394e2c5d..16e7d7a6f9 100644
--- a/theories/Init.v
+++ b/theories/Init.v
@@ -8,8 +8,6 @@
 
 Declare ML Module "ltac2_plugin".
 
-Global Set Default Proof Mode "Ltac2".
-
 (** Primitive types *)
 
 Ltac2 Type int.