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.ml | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) (limited to 'library/goptions.ml') diff --git a/library/goptions.ml b/library/goptions.ml index b5a8b00ea..95259c9b5 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -22,15 +22,9 @@ open Mod_subst (****************************************************************************) (* 0- Common things *) -type option_name = - | PrimaryTable of string - | SecondaryTable of string * string - | TertiaryTable of string * string * string - -let nickname = function - | PrimaryTable s -> s - | SecondaryTable (s1,s2) -> s1^" "^s2 - | TertiaryTable (s1,s2,s3) -> s1^" "^s2^" "^s3 +type option_name = string list + +let nickname table = String.concat " " table let error_undeclared_key key = error ((nickname key)^": no table or option of this type") -- cgit v1.2.3