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

1 files changed, 9 insertions, 1 deletions

diff --git a/lib/util.ml b/lib/util.ml
index c4229fd32..e6c76f7f3 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -699,7 +699,7 @@ let list_split_when p =
   split_when_loop []
 
 (* [list_split_by p l] splits [l] into two lists [(l1,l2)] such that elements of
-   [l1] satisfy [p] and elements of [l2] do not *)
+   [l1] satisfy [p] and elements of [l2] do not; order is preserved *)
 let list_split_by p =
   let rec split_by_loop = function
   | []   -> ([],[])
@@ -858,6 +858,14 @@ let rec list_cartesians_filter op init ll =
 
 let rec list_drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: list_drop_last tl
 
+(* Factorize lists of pairs according to the left argument *)
+let rec list_factorize_left = function
+  | (a,b)::l ->
+      let al,l' = list_split_by (fun (a',b) -> a=a') l in
+      (a,(b::List.map snd al)) :: list_factorize_left l'
+  | [] ->
+      []
+
 (* Arrays *)
 
 let array_compare item_cmp v1 v2 =