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/usage.ml')

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