diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index afd017bed3..a32f6b8a1e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -741,7 +741,7 @@ let _ = let _ = declare_bool_option - { optsync = true; + { optsync = false; (* synchronisation is in Impargs *) optname = "strict implicits"; optkey = (SecondaryTable ("Strict","Implicits")); optread = Impargs.is_strict_implicit_args; |