From 2d0e7cca0227a935b43e8afe08330af8d7c3a5c3 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 18 Mar 2012 13:56:55 +0000 Subject: Fixing bug #2732 (anomaly when using the tolerance for writing "f atomic_tac" as a short-hand for "f ltac:(atomic_tac)" for "f" an Ltac function - see Tacinterp.add_primitive_tactic). More precisely, when parsing "f ref" and "ref" is recognized as the name of some TACTIC-EXTEND-defined tactic parsable as an atomic tactic (like "eauto", "firstorder", "discriminate", ...), the code was correct only when a rule of the form `TACTIC EXTEND ... [ "foo" -> ...] END' was given (where "foo" has no arguments in the rule) but not when a rule of the form `TACTIC EXTEND ... [ "foo" tactic_opt(p) -> ...] END' was given (where "foo" had an optional argument in the rule). In particular, "firstorder" was in this case. More generally, if, for an extra argument able to parse the empty string, a rule `TACTIC EXTEND ... [ "foo" my_special_extra_arg(p) -> ...] END' was given, then "foo" was not recognized as parseable as an atomic string (this happened e.g. for "eauto"). This is now also fixed. There was also another bug when the internal name of tactic was not the same as the user-level name of the tactic. This is the reason why "congruence" was not recognized when given as argument of an ltac (its internal name is "cc"). Incidentally removed the redundant last line in the parsing rule for "firstorder". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15041 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/genarg.mli | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'interp/genarg.mli') diff --git a/interp/genarg.mli b/interp/genarg.mli index 9c47c691a..43cd73aed 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -257,7 +257,8 @@ val app_pair : (** create a new generic type of argument: force to associate unique ML types at each of the three levels *) -val create_arg : string -> +val create_arg : 'globa option -> + string -> ('a,tlevel) abstract_argument_type * ('globa,glevel) abstract_argument_type * ('rawa,rlevel) abstract_argument_type @@ -299,7 +300,6 @@ val in_gen : val out_gen : ('a,'co) abstract_argument_type -> 'co generic_argument -> 'a - (** [in_generic] is used in combination with camlp4 [Gramext.action] magic [in_generic: !l:type, !a:argument_type -> |a|_l -> 'l generic_argument] @@ -313,3 +313,5 @@ type an_arg_of_this_type val in_generic : argument_type -> an_arg_of_this_type -> 'co generic_argument + +val default_empty_value : ('a,glevel) abstract_argument_type -> 'a option -- cgit v1.2.3