From 102d2db3ea7a7354de5e019224e2778fe7603b8e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 21 Nov 2016 07:25:30 +0100
Subject: Stop parsing -compat-notations options, which are no longer supported
 (bug #3339).

---
 toplevel/usage.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'toplevel')

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\
-- 
cgit v1.2.3


From a27ac0315dcbb99c64a260bac3988199a26b39cf Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 24 Nov 2016 15:14:19 +0100
Subject: Fix some documentation typos.

Note: "dependant" does exist, but it is a noun and it means a person that
is somehow financially dependent on someone else.
---
 toplevel/vernacentries.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 230e62607a..41ee165ff8 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1127,7 +1127,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
@@ -2135,7 +2135,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
-- 
cgit v1.2.3