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, 30 insertions, 30 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 2d7dd9d6c7..418980c54b 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -31,7 +31,7 @@ let _=
   let gdopt=
     { optsync=true;
       optname="Congruence Verbose";
-      optkey=SecondaryTable("Congruence","Verbose"); 
+      optkey=["Congruence";"Verbose"]; 
       optread=(fun ()-> !cc_verbose); 
       optwrite=(fun b -> cc_verbose := b)}  
   in
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
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index d7c5b66ae7..96c5bcae4f 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -30,7 +30,7 @@ let _=
   let gdopt=
     { optsync=true;
       optname="Firstorder Depth";
-      optkey=SecondaryTable("Firstorder","Depth"); 
+      optkey=["Firstorder";"Depth"]; 
       optread=(fun ()->Some !ground_depth); 
       optwrite=
    (function 
@@ -45,7 +45,7 @@ let _=
   let gdopt=
     { optsync=true;
       optname="Congruence Depth";
-      optkey=SecondaryTable("Congruence","Depth"); 
+      optkey=["Congruence";"Depth"]; 
       optread=(fun ()->Some !congruence_depth); 
       optwrite=
    (function 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 69cc0607b6..b29bdf3f16 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -495,7 +495,7 @@ let function_debug_sig =
   {
     optsync = false;
     optname = "Function debug";
-    optkey =  PrimaryTable("Function_debug");
+    optkey =  ["Function_debug"];
     optread = (fun () -> !function_debug);
     optwrite = (fun b -> function_debug := b)
   }
@@ -514,7 +514,7 @@ let strict_tcc_sig =
   {
     optsync = false;
     optname = "Raw Function Tcc";
-    optkey =  PrimaryTable("Function_raw_tcc");
+    optkey =  ["Function_raw_tcc"];
     optread = (fun () -> !strict_tcc);
     optwrite = (fun b -> strict_tcc := b)
   }
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index 6f9e673a92..bff8cae260 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -404,7 +404,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | CPrim (_, String _) -> xlate_error "CPrim (String): TODO"
    | CHole _ -> CT_existvarc 
 (* I assume CDynamic has been inserted to make free form extension of
-   the language possible, but this would go agains the logic of pcoq anyway. *)
+   the language possible, but this would go against the logic of pcoq anyway. *)
    | CDynamic (_, _) -> assert false
    | CDelimiters (_, key, num) -> 
 	 CT_num_encapsulator(CT_num_type key , xlate_formula  num)
@@ -2179,21 +2179,21 @@ let rec xlate_vernac =
   | VernacLocate(LocateNotation s) -> CT_locate_notation(CT_string s)
   | VernacTime(v) -> CT_time(xlate_vernac v)
   | VernacTimeout(n,v) -> CT_timeout(CT_int n,xlate_vernac v)
-  | VernacSetOption (Goptions.SecondaryTable ("Implicit", "Arguments"), BoolValue true)->CT_user_vernac (CT_ident "IMPLICIT_ARGS_ON", CT_varg_list[])
+  | VernacSetOption (["Implicit"; "Arguments"], BoolValue true)->CT_user_vernac (CT_ident "IMPLICIT_ARGS_ON", CT_varg_list[])
   |VernacExactProof f -> CT_proof(xlate_formula f)
   | VernacSetOption (table, BoolValue true) -> 
       let table1 = 
 	match table with
-	    PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
-	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2)
-	  | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in
+	    [s] -> CT_coerce_ID_to_TABLE(CT_ident s)
+	  | [s1;s2] -> CT_table(CT_ident s1, CT_ident s2)
+	  | _ -> xlate_error "TODO: arbitrary-length Table names" in
 	CT_set_option(table1)
   | VernacSetOption (table, v) -> 
       let table1 = 
 	match table with
-	    PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
-	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2)
-	  | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in
+	    [s] -> CT_coerce_ID_to_TABLE(CT_ident s)
+	  | [s1;s2] -> CT_table(CT_ident s1, CT_ident s2)
+	  | _ -> xlate_error "TODO: arbitrary-length Table names" in
       let value =
 	match v with
 	  | BoolValue _ -> assert false
@@ -2205,9 +2205,9 @@ let rec xlate_vernac =
   | VernacUnsetOption(table) ->
       let table1 = 
 	match table with
-	    PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
-	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2)
-	  | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in
+	    [s] -> CT_coerce_ID_to_TABLE(CT_ident s)
+	  | [s1;s2] -> CT_table(CT_ident s1, CT_ident s2)
+	  | _ -> xlate_error "TODO: arbitrary-length Table names" in
 	CT_unset_option(table1)
   | VernacAddOption (table, l) ->
       let values =
@@ -2221,9 +2221,9 @@ let rec xlate_vernac =
 	match values with [] -> assert false | a::b -> (a,b) in
       let table1 = 
 	match table with
-	    PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
-	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2)
-	  | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in
+	    [s] -> CT_coerce_ID_to_TABLE(CT_ident s)
+	  | [s1;s2] -> CT_table(CT_ident s1, CT_ident s2)
+	  | _ -> xlate_error "TODO: arbitrary-length Table names" in
 	CT_set_option_value2(table1, CT_id_or_string_ne_list(fst, values1))
   | VernacImport(true, a::l) ->
       CT_export_id(CT_id_ne_list(reference_to_ct_ID a,
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 5354598853..8c8640ea53 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -61,7 +61,7 @@ let _ =
   declare_bool_option 
     { optsync  = false;
       optname  = "Omega system time displaying flag";
-      optkey   = SecondaryTable ("Omega","System");
+      optkey   = ["Omega";"System"];
       optread  = read display_system_flag;
       optwrite = write display_system_flag }
 
@@ -69,7 +69,7 @@ let _ =
   declare_bool_option 
     { optsync  = false;
       optname  = "Omega action display flag";
-      optkey   = SecondaryTable ("Omega","Action");
+      optkey   = ["Omega";"Action"];
       optread  = read display_action_flag;
       optwrite = write display_action_flag }
 
@@ -77,7 +77,7 @@ let _ =
   declare_bool_option 
     { optsync  = false;
       optname  = "Omega old style flag";
-      optkey   = SecondaryTable ("Omega","OldStyle");
+      optkey   = ["Omega";"OldStyle"];
       optread  = read old_style_flag;
       optwrite = write old_style_flag }
 
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 9d9d66bb28..1fee72a601 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -50,7 +50,7 @@ let pruning = ref true
 let opt_pruning=
   {optsync=true;
    optname="Rtauto Pruning";
-   optkey=SecondaryTable("Rtauto","Pruning");
+   optkey=["Rtauto";"Pruning"];
    optread=(fun () -> !pruning);
    optwrite=(fun b -> pruning:=b)}
 
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 6cde1ddcf5..b47bbaa93f 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -245,7 +245,7 @@ let verbose = ref false
 let opt_verbose=
   {optsync=true;
    optname="Rtauto Verbose";
-   optkey=SecondaryTable("Rtauto","Verbose");
+   optkey=["Rtauto";"Verbose"];
    optread=(fun () -> !verbose);
    optwrite=(fun b -> verbose:=b)}
 
@@ -256,7 +256,7 @@ let check = ref false
 let opt_check=
   {optsync=true;
    optname="Rtauto Check";
-   optkey=SecondaryTable("Rtauto","Check");
+   optkey=["Rtauto";"Check"];
    optread=(fun () -> !check);
    optwrite=(fun b -> check:=b)}
 
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index a54b3a86ff..a8f5815bc5 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -77,7 +77,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "transparency of Program obligations";
-      optkey   = (SecondaryTable ("Transparent","Obligations"));
+      optkey   = ["Transparent";"Obligations"];
       optread  = get_proofs_transparency;
       optwrite = set_proofs_transparency; }