From 4e20ed9e5c1608226f0d736df10bb82fc402e7a2 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 23 Oct 2013 22:17:16 +0000
Subject: 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
---
 grammar/tacextend.ml4 | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'grammar')

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 5ea514174b..12de0bcbe8 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
-- 
cgit v1.2.3