From d2d1fe30e3defa18dd966bf8160df81fc1e72e31 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 9 Mar 2018 10:27:39 -0300
Subject: Fix compilation after the change of API in options.

---
 src/tac2entries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index fa498ab44f..1631880c71 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -919,7 +919,7 @@ 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"
+  Goptions.set_string_option_value_gen ["Default"; "Proof"; "Mode"] "Ltac2"
 
 (** Dummy object that register global rules when Require is called *)
 let inTac2Init : unit -> obj =
-- 
cgit v1.2.3