aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
diff options
context:
space:
mode:
Diffstat (limited to 'grammar')
-rw-r--r--grammar/tacextend.ml45
1 files changed, 3 insertions, 2 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