diff options
| author | Pierre-Marie Pédrot | 2016-11-30 22:47:38 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-11-30 22:47:38 +0100 |
| commit | cf8ecf83b5cc52f7ea73dc1d3af59bf03deff688 (patch) | |
| tree | bd5a6ad80bb09684899fbcc66963d39ae9a9b52a /toplevel | |
| parent | 88b2eb9279bf5f83f27057094de5b696ee9916e3 (diff) | |
| parent | 3e6fa1cbdc0ec145728089000595b6ea29f37a4c (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/usage.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
2 files changed, 2 insertions, 4 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 956a402617..38ceacf5ec 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -36,8 +36,6 @@ let print_usage_channel co command = \n -noinit start without loading the Init library\ \n -nois (idem)\ \n -compat X.Y provides compatibility support for Coq version X.Y\ -\n -verbose-compat-notations be warned when using compatibility notations\ -\n -no-compat-notations get an error when using compatibility notations\ \n\ \n -load-ml-object f load ML object file f\ \n -load-ml-source f load ML file f\ diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index cd61bf7ff3..8ce13c69af 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1128,7 +1128,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags (* Parts of this code are overly complicated because the implicit arguments API is completely crazy: positions (ExplByPos) are elaborated to names. This is broken by design, since not all arguments have names. So - eventhough we eventually want to map only positions to implicit statuses, + even though we eventually want to map only positions to implicit statuses, we have to check whether the corresponding arguments have names, not to trigger an error in the impargs code. Even better, the names we have to check are not the current ones (after previous renamings), but the original @@ -2136,7 +2136,7 @@ let enforce_polymorphism = function | None -> Flags.is_universe_polymorphism () | Some b -> Flags.make_polymorphic_flag b; b -(** A global default timeout, controled by option "Set Default Timeout n". +(** A global default timeout, controlled by option "Set Default Timeout n". Use "Unset Default Timeout" to deactivate it (or set it to 0). *) let default_timeout = ref None |