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

1 files changed, 4 insertions, 4 deletions

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index f1e8f42fe6..83a780198a 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -327,7 +327,7 @@ let auto_inline () = !auto_inline_ref
 let _ = declare_bool_option
 	  {optsync = true;
 	   optname = "Extraction AutoInline";
-	   optkey = SecondaryTable ("Extraction", "AutoInline");
+	   optkey = ["Extraction"; "AutoInline"];
 	   optread = auto_inline;
 	   optwrite = (:=) auto_inline_ref}
 
@@ -340,7 +340,7 @@ let type_expand () = !type_expand_ref
 let _ = declare_bool_option
 	  {optsync = true;
 	   optname = "Extraction TypeExpand";
-	   optkey = SecondaryTable ("Extraction", "TypeExpand");
+	   optkey = ["Extraction"; "TypeExpand"];
 	   optread = type_expand;
 	   optwrite = (:=) type_expand_ref}
 
@@ -389,14 +389,14 @@ let optims () = !opt_flag_ref
 let _ = declare_bool_option
 	  {optsync = true;
 	   optname = "Extraction Optimize";
-	   optkey = SecondaryTable ("Extraction", "Optimize");
+	   optkey = ["Extraction"; "Optimize"];
 	   optread = (fun () -> !int_flag_ref <> 0);
 	   optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))}
 
 let _ = declare_int_option
           { optsync = true;
             optname = "Extraction Flag";
-            optkey = SecondaryTable("Extraction","Flag");
+            optkey = ["Extraction";"Flag"];
             optread = (fun _ -> Some !int_flag_ref);
             optwrite = (function
                           | None -> chg_flag 0