From 2435a02751df1818977ce58ddf21a8f12ed87be6 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 18 Mar 2012 15:34:15 +0000 Subject: 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 --- lib/util.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'lib/util.ml') 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 = -- cgit v1.2.3