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, 13 insertions, 23 deletions

diff --git a/library/goptions.mli b/library/goptions.mli
index 53f6a6cdb..aefddbbda 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -15,11 +15,12 @@
    - Variables storing options value are created by applying one of the
    [declare_int_option], [declare_bool_option], ... functions.
 
-   Each table/option is uniquely identified by a key of type [option_name].
-   There are two kinds of table/option idenfiers: the primary ones
-   (supposed to be more global) and the secondary ones
+   Each table/option is uniquely identified by a key of type [option_name]
+   which consists in a list of strings. Note that for parsing constraints, 
+   table names must not be made of more than 2 strings while option names
+   can be of arbitrary length.
 
-   The declaration of a table, say of name [SecondaryTable("Toto","Titi")] 
+   The declaration of a table, say of name [["Toto";"Titi"]] 
    automatically makes available the following vernacular commands:
 
       Add Toto Titi foo.
@@ -28,26 +29,18 @@
       Test Toto Titi.
 
    The declaration of a non boolean option value, say of name
-   [SecondaryTable("Tata","Tutu")], automatically makes available the
+   [["Tata";"Tutu";"Titi"]], automatically makes available the
    following vernacular commands:
 
-       Set Tata Tutu val.
-       Print Table Tata Tutu.
+       Set Tata Tutu Titi val.
+       Print Table Tata Tutu Titi.
 
    If it is the declaration of a boolean value, the following
    vernacular commands are made available:
 
-       Set Tata Tutu.
-       Unset Tata Tutu.
-       Print Table Tata Tutu. (* synonym: Test Table Tata Tutu. *)
-
-   For a primary table, say of name [PrimaryTable("Bidule")], the
-   vernacular commands look like
-
-      Add Bidule foo.
-      Print Table Bidule foo.
-      Set Bidule foo.
-      ...
+       Set Tata Tutu Titi.
+       Unset Tata Tutu Titi.
+       Print Table Tata Tutu Titi. (* synonym: Test Table Tata Tutu Titi. *)
 
    The created table/option may be declared synchronous or not
    (synchronous = consistent with the resetting commands)                   *)
@@ -64,11 +57,8 @@ open Mod_subst
 
 (*s Things common to tables and options. *)
 
-(* The type of primary or secondary table/option keys *)
-type option_name =
-  | PrimaryTable of string
-  | SecondaryTable of string * string
-  | TertiaryTable of string * string * string
+(* The type of table/option keys *)
+type option_name = string list
 
 val error_undeclared_key : option_name -> 'a