From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 20 Aug 2012 18:27:01 +0200
Subject: Imported Upstream version 8.4dfsg

---
 toplevel/coqtop.ml | 21 ++++++++++++---------
 1 file changed, 12 insertions(+), 9 deletions(-)

(limited to 'toplevel/coqtop.ml')

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a60e0d82..df388d1d 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -119,13 +119,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" -> warning "Compatibility with version 8.1 not supported."
-  | "8.0" -> warning "Compatibility with version 8.0 not supported."
-  | s -> error ("Unknown compatibility version \""^s^"\".")
-
 (*s options for the virtual machine *)
 
 let boxed_val = ref false
@@ -152,6 +145,9 @@ let warning s = msg_warning (str 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
@@ -243,9 +239,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 ()
 
+    | "-verbose-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();
@@ -332,6 +332,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 ();
-- 
cgit v1.2.3