Changed the way to support compatibility with previous versions.

Compatibility version is now a global parameter that every feature can
individually browse. This avoids having to keep the names of options
synchronous in their respective files and in now-removed file coqcompat.ml.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12372 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 7 insertions, 54 deletions

diff --git a/toplevel/coqcompat.ml b/toplevel/coqcompat.ml
deleted file mode 100644
index b2c1ea23b..000000000
--- a/toplevel/coqcompat.ml
+++ /dev/null
@@ -1,34 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id$ *)
-
-(* File initially created by Hugo Herbelin, Aug 2009 *)
-
-(* This file centralizes the support for compatibility with previous
-   versions of Coq *)
-
-open Pp
-open Util
-open Goptions
-
-let set_compat_options = function
-  | "8.2" ->
-      set_bool_option_value ["Tactic";"Evars";"Pattern";"Unification"] false;
-      set_bool_option_value ["Discriminate";"Introduction"] false;
-      set_bool_option_value ["Intuition";"Iff";"Unfolding"] true;
-      set_bool_option_value ["Dependent";"Propositions";"Elimination"] false;
-
-  | "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^"\".")
diff --git a/toplevel/coqcompat.mli b/toplevel/coqcompat.mli
deleted file mode 100644
index 59b249829..000000000
--- a/toplevel/coqcompat.mli
+++ /dev/null
@@ -1,11 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id$ *)
-
-val set_compat_options : string -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index d66e975fc..e00c56a14 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -121,6 +121,12 @@ let compile_files () =
 	   Vernac.compile v f)
       (List.rev !compile_list)
 
+let set_compat_version = function
+  | "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^"\".")
+
 let re_exec_version = ref ""
 let set_byte () = re_exec_version := "byte"
 let set_opt () = re_exec_version := "opt"
@@ -163,12 +169,6 @@ let set_vm_opt () =
   Flags.set_boxed_definitions !boxed_def;
   Vconv.set_use_vm !use_vm
 
-(*s Compatibility options *)
-
-let compat_version = ref None
-let set_compat_options () =
-  Option.iter Coqcompat.set_compat_options !compat_version
-
 (*s Parsing of the command line.
     We no longer use [Arg.parse], in order to use share [Usage.print_usage]
     between coqtop and coqc. *)
@@ -273,7 +273,7 @@ let parse_args is_ide =
 
     | "-debug" :: rem -> set_debug (); parse rem
 
-    | "-compat" :: v :: rem -> compat_version := Some v; parse rem
+    | "-compat" :: v :: rem -> set_compat_version v; parse rem
     | "-compat" :: []       -> usage ()
 
     | "-vm" :: rem -> use_vm := true; parse rem
@@ -350,7 +350,6 @@ let init is_ide =
       init_load_path ();
       inputstate ();
       set_vm_opt ();
-      set_compat_options ();
       engage ();
       if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then
         Option.iter Declaremods.start_library !toplevel_name;
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 7f759cad9..13b27d5ab 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -21,5 +21,4 @@ Protectedtoplevel
 Toplevel
 Usage
 Coqinit
-Coqcompat
 Coqtop