From 5892f94fd5ca3a269e51eec26c3ff8f616ce02bd Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 6 Oct 2016 11:19:35 +0200
Subject: Remove the -no-compat-notations flag.

This option was not doing anything... Today, one can turn the
compatibility notations warning into an error, if ever that was the
intended semantics.
---
 toplevel/coqtop.ml | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index cf0efca69d..ebdf804ba0 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -332,8 +332,6 @@ let error_missing_arg s =
 let filter_opts = ref false
 let exitcode () = if !filter_opts then 2 else 0
 
-let no_compat_ntn = ref false
-
 let print_where = ref false
 let print_config = ref false
 let print_tags = ref false
@@ -557,7 +555,6 @@ let parse_args arglist =
     |"-just-parsing" -> Vernac.just_parsing := true
     |"-m"|"--memory" -> memory_stat := true
     |"-noinit"|"-nois" -> load_init := false
-    |"-no-compat-notations" -> no_compat_ntn := true
     |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true
     |"-native-compiler" ->
       if Coq_config.no_native_compiler then
-- 
cgit v1.2.3