Improved parameterization of Coq:

- add coqtop option "-compat X.Y" so as to provide compatibility with
  previous versions of Coq (of course, this requires to take care of
  providing flags for controlling changes of behaviors!),
- add support for option names made of an arbitrary length of words
  (instead of one, two or three words only),
- add options for recovering 8.2 behavior for discriminate, tauto,
  evar unification ("Set Tactic Evars Pattern Unification", "Set
  Discriminate Introduction", "Set Intuition Iff Unfolding").

Update of .gitignore

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

9 files changed, 112 insertions, 54 deletions

diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 520f9b6311..29bef7b5a3 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -310,7 +310,7 @@ let end_autoinstance () =
 let _ =
   Goptions.declare_bool_option
     { Goptions.optsync=true;
-      Goptions.optkey=Goptions.PrimaryTable("Autoinstance");
+      Goptions.optkey=["Autoinstance"];
       Goptions.optname="automatic typeclass instance recognition";
       Goptions.optread=(fun () -> !autoinstance_opt);
       Goptions.optwrite=(fun b -> if b then begin_autoinstance() else end_autoinstance()) }
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7d615028ee..48a5119d15 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -272,7 +272,7 @@ let _ =
   declare_bool_option
     { optsync  = true;
       optname  = "automatic declaration of boolean equality";
-      optkey   = (SecondaryTable ("Equality","Scheme"));
+      optkey   = ["Equality";"Scheme"];
       optread  = (fun () -> !eq_flag) ;
       optwrite = (fun b -> eq_flag := b) }
 
@@ -640,7 +640,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "automatic declaration of eliminations";
-      optkey   = (SecondaryTable ("Elimination","Schemes"));
+      optkey   = ["Elimination";"Schemes"];
       optread  = (fun () -> !elim_flag) ;
       optwrite = (fun b -> elim_flag := b) }
 
diff --git a/toplevel/coqcompat.ml b/toplevel/coqcompat.ml
new file mode 100644
index 0000000000..8bf1e9bd00
--- /dev/null
+++ b/toplevel/coqcompat.ml
@@ -0,0 +1,33 @@
+(************************************************************************)
+(*  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
+
+  | "8.1" ->
+      warning "Compatibility with versions 8.1 not supported."
+
+  | "8.0" ->
+      warning "Compatibility with versions 8.0 not supported."
+
+  | s ->
+      error ("Unknown compatibility version \""^s^"\".")
diff --git a/toplevel/coqcompat.mli b/toplevel/coqcompat.mli
new file mode 100644
index 0000000000..59b2498293
--- /dev/null
+++ b/toplevel/coqcompat.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*  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 696ce12826..a699e528b0 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -163,6 +163,12 @@ 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. *)
@@ -267,6 +273,9 @@ let parse_args is_ide =
 
     | "-debug" :: rem -> set_debug (); parse rem
 
+    | "-compat" :: v :: rem -> compat_version := Some v; parse rem
+    | "-compat" :: []       -> usage ()
+
     | "-vm" :: rem -> use_vm := true; parse rem
     | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem
     | "-emacs-U" :: rem -> Flags.print_emacs := true; 
@@ -293,7 +302,9 @@ let parse_args is_ide =
     | "-user" :: u :: rem -> set_rcuser u; parse rem
     | "-user" :: []       -> usage ()
 
-    | "-notactics" :: rem -> remove_top_ml (); parse rem
+    | "-notactics" :: rem -> 
+	warning "Obsolete option \"-notactics\".";
+	remove_top_ml (); parse rem
 
     | "-just-parsing" :: rem -> Vernac.just_parsing := true; parse rem
 
@@ -339,6 +350,7 @@ 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 13b27d5abc..7f759cad9c 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -21,4 +21,5 @@ Protectedtoplevel
 Toplevel
 Usage
 Coqinit
+Coqcompat
 Coqtop
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 8a8480c416..fcb14b2c64 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -33,6 +33,7 @@ let print_usage_channel co command =
   -is f                  (idem)
   -nois                  start with an empty state
   -outputstate f         write state in file f.coq
+  -compat X.Y            provides compatibility support for Coq version X.Y
 
   -load-ml-object f      load ML object file f 
   -load-ml-source f      load ML file f 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5d76f4ff20..fa56e60f69 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -785,7 +785,7 @@ let _ =
   declare_bool_option 
     { optsync  = false;
       optname  = "silent";
-      optkey   = (PrimaryTable "Silent");
+      optkey   = ["Silent"];
       optread  = is_silent;
       optwrite = make_silent_if_not_pcoq }
 
@@ -793,7 +793,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "implicit arguments";
-      optkey   = (SecondaryTable ("Implicit","Arguments"));
+      optkey   = ["Implicit";"Arguments"];
       optread  = Impargs.is_implicit_args;
       optwrite = Impargs.make_implicit_args }
 
@@ -801,7 +801,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "strict implicit arguments";
-      optkey   = (SecondaryTable ("Strict","Implicit"));
+      optkey   = ["Strict";"Implicit"];
       optread  = Impargs.is_strict_implicit_args;
       optwrite = Impargs.make_strict_implicit_args }
 
@@ -809,7 +809,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "strong strict implicit arguments";
-      optkey   = (TertiaryTable ("Strongly","Strict","Implicit"));
+      optkey   = ["Strongly";"Strict";"Implicit"];
       optread  = Impargs.is_strongly_strict_implicit_args;
       optwrite = Impargs.make_strongly_strict_implicit_args }
 
@@ -817,7 +817,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "contextual implicit arguments";
-      optkey   = (SecondaryTable ("Contextual","Implicit"));
+      optkey   = ["Contextual";"Implicit"];
       optread  = Impargs.is_contextual_implicit_args;
       optwrite = Impargs.make_contextual_implicit_args }
 
@@ -825,7 +825,7 @@ let _ =
 (*   declare_bool_option  *)
 (*     { optsync  = true; *)
 (*       optname  = "forceable implicit arguments"; *)
-(*       optkey   = (SecondaryTable ("Forceable","Implicit")); *)
+(*       optkey   = ["Forceable";"Implicit")); *)
 (*       optread  = Impargs.is_forceable_implicit_args; *)
 (*       optwrite = Impargs.make_forceable_implicit_args } *)
 
@@ -833,7 +833,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "implicit status of reversible patterns";
-      optkey   = (TertiaryTable ("Reversible","Pattern","Implicit"));
+      optkey   = ["Reversible";"Pattern";"Implicit"];
       optread  = Impargs.is_reversible_pattern_implicit_args;
       optwrite = Impargs.make_reversible_pattern_implicit_args }
 
@@ -841,7 +841,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "maximal insertion of implicit";
-      optkey   = (TertiaryTable ("Maximal","Implicit","Insertion"));
+      optkey   = ["Maximal";"Implicit";"Insertion"];
       optread  = Impargs.is_maximal_implicit_args;
       optwrite = Impargs.make_maximal_implicit_args }
 
@@ -849,7 +849,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "coercion printing";
-      optkey   = (SecondaryTable ("Printing","Coercions"));
+      optkey   = ["Printing";"Coercions"];
       optread  = (fun () -> !Constrextern.print_coercions);
       optwrite = (fun b ->  Constrextern.print_coercions := b) }
 
@@ -857,14 +857,14 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "printing of existential variable instances";
-      optkey   = (TertiaryTable ("Printing","Existential","Instances"));
+      optkey   = ["Printing";"Existential";"Instances"];
       optread  = (fun () -> !Constrextern.print_evar_arguments);
       optwrite = (:=) Constrextern.print_evar_arguments }
 let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "implicit arguments printing";
-      optkey   = (SecondaryTable ("Printing","Implicit"));
+      optkey   = ["Printing";"Implicit"];
       optread  = (fun () -> !Constrextern.print_implicits);
       optwrite = (fun b ->  Constrextern.print_implicits := b) }
 
@@ -872,7 +872,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "implicit arguments defensive printing";
-      optkey   = (TertiaryTable ("Printing","Implicit","Defensive"));
+      optkey   = ["Printing";"Implicit";"Defensive"];
       optread  = (fun () -> !Constrextern.print_implicits_defensive);
       optwrite = (fun b ->  Constrextern.print_implicits_defensive := b) }
 
@@ -880,7 +880,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "projection printing using dot notation";
-      optkey   = (SecondaryTable ("Printing","Projections"));
+      optkey   = ["Printing";"Projections"];
       optread  = (fun () -> !Constrextern.print_projections);
       optwrite = (fun b ->  Constrextern.print_projections := b) }
 
@@ -888,7 +888,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "notations printing";
-      optkey   = (SecondaryTable ("Printing","Notations"));
+      optkey   = ["Printing";"Notations"];
       optread  = (fun () -> not !Constrextern.print_no_symbol);
       optwrite = (fun b ->  Constrextern.print_no_symbol := not b) }
 
@@ -896,7 +896,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "raw printing";
-      optkey   = (SecondaryTable ("Printing","All"));
+      optkey   = ["Printing";"All"];
       optread  = (fun () -> !Flags.raw_print);
       optwrite = (fun b -> Flags.raw_print := b) }
 
@@ -904,7 +904,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "use of virtual machine inside the kernel";
-      optkey   = (SecondaryTable ("Virtual","Machine"));
+      optkey   = ["Virtual";"Machine"];
       optread  = (fun () -> Vconv.use_vm ());
       optwrite = (fun b -> Vconv.set_use_vm b) }
 
@@ -912,7 +912,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "use of boxed definitions";
-      optkey   = (SecondaryTable ("Boxed","Definitions"));
+      optkey   = ["Boxed";"Definitions"];
       optread  = Flags.boxed_definitions;
       optwrite = (fun b -> Flags.set_boxed_definitions b) } 
 
@@ -920,60 +920,60 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "use of boxed values";
-      optkey   = (SecondaryTable ("Boxed","Values"));
+      optkey   = ["Boxed";"Values"];
       optread  = (fun _ -> not (Vm.transp_values ()));
       optwrite = (fun b -> Vm.set_transp_values (not b)) } 
 
 let _ =
   declare_int_option
-    { optsync=false;
-      optkey=PrimaryTable("Undo");
-      optname="the undo limit";
-      optread=Pfedit.get_undo;
-      optwrite=Pfedit.set_undo }
+    { optsync  = false;
+      optname  = "the undo limit";
+      optkey   = ["Undo"];
+      optread  = Pfedit.get_undo;
+      optwrite = Pfedit.set_undo }
 
 let _ =
   declare_int_option
-    { optsync=false;
-      optkey=SecondaryTable("Hyps","Limit");
-      optname="the hypotheses limit";
-      optread=Flags.print_hyps_limit;
-      optwrite=Flags.set_print_hyps_limit }
+    { optsync  = false;
+      optname  = "the hypotheses limit";
+      optkey   = ["Hyps";"Limit"];
+      optread  = Flags.print_hyps_limit;
+      optwrite = Flags.set_print_hyps_limit }
 
 let _ =
   declare_int_option
-    { optsync=true;
-      optkey=SecondaryTable("Printing","Depth");
-      optname="the printing depth";
-      optread=Pp_control.get_depth_boxes;
-      optwrite=Pp_control.set_depth_boxes }
+    { optsync  = true;
+      optname  = "the printing depth";
+      optkey   = ["Printing";"Depth"];
+      optread  = Pp_control.get_depth_boxes;
+      optwrite = Pp_control.set_depth_boxes }
 
 let _ =
   declare_int_option
-    { optsync=true;
-      optkey=SecondaryTable("Printing","Width");
-      optname="the printing width";
-      optread=Pp_control.get_margin;
-      optwrite=Pp_control.set_margin }
+    { optsync  = true;
+      optname  = "the printing width";
+      optkey   = ["Printing";"Width"];
+      optread  = Pp_control.get_margin;
+      optwrite = Pp_control.set_margin }
 
 let _ =
   declare_bool_option
-    { optsync=true;
-      optkey=SecondaryTable("Printing","Universes");
-      optname="printing of universes";
-      optread=(fun () -> !Constrextern.print_universes);
-      optwrite=(fun b -> Constrextern.print_universes:=b) }
+    { optsync  = true;
+      optname  = "printing of universes";
+      optkey   = ["Printing";"Universes"];
+      optread  = (fun () -> !Constrextern.print_universes);
+      optwrite = (fun b -> Constrextern.print_universes:=b) }
 
 let vernac_debug b =
   set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
 
 let _ =
   declare_bool_option
-    { optsync=false;
-      optkey=SecondaryTable("Ltac","Debug");
-      optname="Ltac debug";
-      optread=(fun () -> get_debug () <> Tactic_debug.DebugOff);
-      optwrite=vernac_debug }
+    { optsync  = false;
+      optname  = "Ltac debug";
+      optkey   = ["Ltac";"Debug"];
+      optread  = (fun () -> get_debug () <> Tactic_debug.DebugOff);
+      optwrite = vernac_debug }
 
 let vernac_set_opacity local str =
   let glob_ref r =
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 82a2a84495..63d93a7676 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -42,7 +42,7 @@ let _ =
   declare_string_option 
     { optsync  = false;
       optname  = "Whelp server";
-      optkey   = (SecondaryTable ("Whelp","Server"));
+      optkey   = ["Whelp";"Server"];
       optread  = (fun () -> !whelp_server_name);
       optwrite = (fun s -> whelp_server_name := s) }
 
@@ -50,7 +50,7 @@ let _ =
   declare_string_option 
     { optsync  = false;
       optname  = "Whelp getter";
-      optkey   = (SecondaryTable ("Whelp","Getter"));
+      optkey   = ["Whelp";"Getter"];
       optread  = (fun () -> !getter_server_name);
       optwrite = (fun s -> getter_server_name := s) }