From 25dde2366a4db47e5da13b2bbe4d03a31235706f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 2 Aug 2009 19:51:48 +0000
Subject: 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
---
 plugins/extraction/table.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/extraction')

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
-- 
cgit v1.2.3