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

10 files changed, 38 insertions, 61 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index da80130283..971b560ec2 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -37,6 +37,14 @@ let raw_print = ref false
 
 let unicode_syntax = ref false
 
+(* Compatibility mode *)
+
+type compat_version = V8_2
+let compat_version = ref None
+let version_strictly_greater v =
+  match !compat_version with None -> true | Some v' -> v'>v
+let version_less_or_equal v = not (version_strictly_greater v)
+
 (* Translate *)
 let beautify = ref false
 let make_beautify f = beautify := f
diff --git a/lib/flags.mli b/lib/flags.mli
index e8a7819c89..50ba923b74 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -29,6 +29,11 @@ val raw_print : bool ref
 
 val unicode_syntax : bool ref
 
+type compat_version = V8_2
+val compat_version : compat_version option ref
+val version_strictly_greater : compat_version -> bool
+val version_less_or_equal : compat_version -> bool
+
 val beautify : bool ref
 val make_beautify : bool -> unit
 val do_beautify : unit -> bool
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index fe18a0d192..e8d95a7985 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -160,6 +160,7 @@ let default_no_delta_unify_flags = {
 
 let use_evars_pattern_unification flags =
   !global_evars_pattern_unification_flag && flags.use_evars_pattern_unification
+  && Flags.version_strictly_greater Flags.V8_2
 
 let expand_key env = function
   | Some (ConstKey cst) -> constant_opt_value env cst
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 6adfa3aafa..200b6deb71 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -46,7 +46,10 @@ open Evd
 
 (* Options *)
 
-let discr_do_intro = ref true
+let discriminate_introduction = ref true
+
+let discr_do_intro () =
+  !discriminate_introduction && Flags.version_strictly_greater Flags.V8_2
 
 open Goptions
 let _ =
@@ -54,8 +57,8 @@ let _ =
     { optsync  = true;
       optname  = "automatic introduction of hypotheses by discriminate";
       optkey   = ["Discriminate";"Introduction"];
-      optread  = (fun () -> !discr_do_intro);
-      optwrite = (:=) discr_do_intro }
+      optread  = (fun () -> !discriminate_introduction);
+      optwrite = (:=) discriminate_introduction }
 
 (* Rewriting tactics *)
 
@@ -683,7 +686,7 @@ let discrEverywhere with_evars =
 (*
   tclORELSE
 *)
-    (if !discr_do_intro then
+    (if discr_do_intro () then
       (tclTHEN
 	(tclREPEAT introf)
 	(Tacticals.tryAllHyps
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2a4fc6a0f5..f4262d731a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -80,6 +80,11 @@ let dloc = dummy_loc
 (* Option for 8.2 compatibility *)
 open Goptions
 let dependent_propositions_elimination = ref true
+
+let use_dependent_propositions_elimination () =
+  !dependent_propositions_elimination
+  && Flags.version_strictly_greater Flags.V8_2
+
 let _ =
   declare_bool_option
     { optsync  = true;
@@ -2581,8 +2586,8 @@ let guess_elim isrec hyp0 gl =
     if isrec then lookup_eliminator mind s
     else
       let case =
-	if !dependent_propositions_elimination &&
-	   dependent_no_evar (mkVar hyp0) (pf_concl gl)
+	if use_dependent_propositions_elimination () &&
+	   dependent_no_evar (mkVar hyp0) (pf_concl gl) 
 	then make_case_dep
 	else make_case_gen in
       pf_apply case gl mind s in
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 6fea983772..60baa017cf 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -49,6 +49,8 @@ let strict_unit = false
 (* Whether inner iff are unfolded *)
 let iff_unfolding = ref false
 
+let unfold_iff () = !iff_unfolding || Flags.version_less_or_equal Flags.V8_2
+
 open Goptions
 let _ =
   declare_bool_option
@@ -256,7 +258,7 @@ let rec tauto_intuit t_reduce solver ist =
    ) >>
 
 let reduction_not _ist =
-  if !iff_unfolding then
+  if unfold_iff () then
     <:tactic< unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in * >>
   else
     <:tactic< unfold Coq.Init.Logic.not in * >>
diff --git a/toplevel/coqcompat.ml b/toplevel/coqcompat.ml
deleted file mode 100644
index b2c1ea23bc..0000000000
--- 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 59b2498293..0000000000
--- 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 d66e975fcf..e00c56a14c 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 7f759cad9c..13b27d5abc 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -21,5 +21,4 @@ Protectedtoplevel
 Toplevel
 Usage
 Coqinit
-Coqcompat
 Coqtop