CList.factorize_left with a parametric equality

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16923 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 15 insertions, 12 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 5ea514174..12de0bcbe 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -172,8 +172,9 @@ let rec possibly_empty_subentries loc = function
 let possibly_atomic loc prods =
   let l = List.map_filter (function
     | GramTerminal s :: l, _, _ -> Some (s,l)
-    | _ -> None) prods in
-  possibly_empty_subentries loc (List.factorize_left l)
+    | _ -> None) prods
+  in
+  possibly_empty_subentries loc (List.factorize_left String.equal l)
 
 let declare_tactic loc s c cl =
   let se = mlexpr_of_string s in
diff --git a/lib/cList.ml b/lib/cList.ml
index e0ac9839f..8fa8c392f 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -135,7 +135,7 @@ sig
   val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
   val cartesians_filter :
     ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
-  val factorize_left : ('a * 'b) list -> ('a * 'b list) list
+  val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list
 
 end
 
@@ -603,7 +603,7 @@ let subset l1 l2 =
 
 let chop n l =
   let rec chop_aux i acc = function
-    | tl when i=0 -> (List.rev acc, tl)
+    | tl when Int.equal i 0 -> (List.rev acc, tl)
     | h::t -> chop_aux (pred i) (h::acc) t
     | [] -> failwith "List.chop"
   in
@@ -641,7 +641,7 @@ let rec last = function
 let lastn n l =
   let len = List.length l in
   let rec aux m l =
-    if m = n then l else aux (m - 1) (List.tl l)
+    if Int.equal m n then l else aux (m - 1) (List.tl l)
   in
   if len < n then failwith "lastn" else aux len l
 
@@ -747,12 +747,14 @@ let cartesians_filter op init ll =
 
 (* Drop the last element of a list *)
 
-let rec drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: drop_last tl
+let rec drop_last = function
+  | [] -> assert false
+  | hd :: [] -> []
+  | hd :: tl -> hd :: drop_last tl
 
 (* Factorize lists of pairs according to the left argument *)
-let rec factorize_left = function
+let rec factorize_left cmp = function
   | (a,b)::l ->
-      let al,l' = partition (fun (a',b) -> a=a') l in (* FIXME *)
-      (a,(b::List.map snd al)) :: factorize_left l'
-  | [] ->
-      []
+      let al,l' = partition (fun (a',_) -> cmp a a') l in
+      (a,(b::List.map snd al)) :: factorize_left cmp l'
+  | [] -> []
diff --git a/lib/cList.mli b/lib/cList.mli
index 013e00173..99d6aab15 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -230,7 +230,7 @@ sig
     ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
   (** Keep only those products that do not return None *)
 
-  val factorize_left : ('a * 'b) list -> ('a * 'b list) list
+  val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list
 end
 
 include ExtS