diff options
| author | Pierre-Marie Pédrot | 2018-03-09 10:27:39 -0300 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-03-09 10:27:39 -0300 |
| commit | d2d1fe30e3defa18dd966bf8160df81fc1e72e31 (patch) | |
| tree | 59eddd1ea50317bbc55f40d0df53aaa38dfec7a8 /src | |
| parent | ba27c2e21f80b41dfd837e6c6b15f82ca405cf04 (diff) | |
Fix compilation after the change of API in options.
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2entries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 = |