diff options
Diffstat (limited to 'toplevel/coqtop.ml')
| -rw-r--r-- | toplevel/coqtop.ml | 19 |
1 files changed, 11 insertions, 8 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 6e5019adb..1a6867a51 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -125,13 +125,6 @@ let compile_files () = Vernac.compile v f) (List.rev !compile_list) -let set_compat_version = function - | "8.3" -> compat_version := Some V8_3 - | "8.2" -> compat_version := Some V8_2 - | "8.1" -> msg_warning (strbrk "Compatibility with version 8.1 not supported.") - | "8.0" -> msg_warning (strbrk "Compatibility with version 8.0 not supported.") - | s -> error ("Unknown compatibility version \""^s^"\".") - (*s options for the virtual machine *) let boxed_val = ref false @@ -158,6 +151,9 @@ let warning s = msg_warning (strbrk s) let ide_slave = ref false let filter_opts = ref false +let verb_compat_ntn = ref false +let no_compat_ntn = ref false + let parse_args arglist = let glob_opt = ref false in let rec parse = function @@ -249,9 +245,13 @@ let parse_args arglist = | "-debug" :: rem -> set_debug (); parse rem - | "-compat" :: v :: rem -> set_compat_version v; parse rem + | "-compat" :: v :: rem -> + Flags.compat_version := get_compat_version v; parse rem | "-compat" :: [] -> usage () + | "-verb-compat-notations" :: rem -> verb_compat_ntn := true; parse rem + | "-no-compat-notations" :: rem -> no_compat_ntn := true; parse rem + | "-vm" :: rem -> use_vm := true; parse rem | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); @@ -342,6 +342,9 @@ let init arglist = Mltop.init_known_plugins (); set_vm_opt (); engage (); + (* Be careful to set these variables after the inputstate *) + Syntax_def.set_verbose_compat_notations !verb_compat_ntn; + Syntax_def.set_compat_notations (not !no_compat_ntn); if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then Option.iter Declaremods.start_library !toplevel_name; init_library_roots (); |