diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-10-06 11:19:35 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-10-06 11:19:35 +0200 |
| commit | 5892f94fd5ca3a269e51eec26c3ff8f616ce02bd (patch) | |
| tree | c67d081aff78b07dabeff224358b3bb266339326 /toplevel | |
| parent | d0dda9c419894460de952d4b9342ea6518d24f83 (diff) | |
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.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index cf0efca69..ebdf804ba 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 |