diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-18 15:34:15 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-18 15:34:15 +0000 |
| commit | 2435a02751df1818977ce58ddf21a8f12ed87be6 (patch) | |
| tree | acefd8322156ff5c9791a8f1a4c210f700eb45d5 /lib/util.mli | |
| parent | 21b90199c995163145daf447f67dd24cbb591e1d (diff) | |
Yet another subtlety with bug 2732: when several grammar rules of a
TACTIC EXTEND block possibly parse the stand-alone name of a tactic,
then only the first rule must be registered in the atomic tactic table
so as to be consistent with what happens when the tactic is invoked
directly via its parsing rules and not via the interpretation of a
reference in the atomic tactic table. Concretely, this affects TACTIC
EXTEND blocks of the form
TACTIC EXTEND foo
[ "bar" tactic_opt(tac) -> ... ]
| [ "bar" constr_list(tac) -> ... ]
where both rules parses "bar" alone but only the first rule must be
registered in the atomic table,
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15046 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/util.mli')
| -rw-r--r-- | lib/util.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/util.mli b/lib/util.mli index 868a76711..37d15792f 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -191,6 +191,7 @@ val list_cartesians_filter : ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list val list_union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b +val list_factorize_left : ('a * 'b) list -> ('a * 'b list) list (** {6 Arrays. } *) |