diff options
| author | herbelin | 2003-04-09 14:42:28 +0000 |
|---|---|---|
| committer | herbelin | 2003-04-09 14:42:28 +0000 |
| commit | 39cd2e369cc4871bf650e4f4f4a667c0e6b4d2d0 (patch) | |
| tree | c356e0b904c568ae95a6ef8e9c18c2b2d2a5914a /toplevel | |
| parent | 713a53132e1332afeb32ec8eadf68ac5a1624951 (diff) | |
Gestion synchronisation des Impargs.*_out et des Impargs._strict dans Impargs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3888 85f007b7-540e-0410-9357-904b9bb8a0f7
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; |