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 --- library/goptions.mli | 36 +++++++++++++----------------------- 1 file changed, 13 insertions(+), 23 deletions(-) (limited to 'library/goptions.mli') 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 -- cgit v1.2.3