aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-09-23 18:56:18 +0200
committerPierre-Marie Pédrot2016-09-23 18:56:18 +0200
commita52d06ea16cff00faa7d2f63ad5c1ca0b58e64b4 (patch)
tree40440d7daed82bd24180b36ef224f245ddca42f5 /parsing
parent30a908becf31d91592a1f7934cfa3df2d67d1834 (diff)
parenta321074cdd2f9375662c7c9f17be5c045328bd82 (diff)
Merge branch 'v8.6'
Diffstat (limited to 'parsing')
-rw-r--r--parsing/egramcoq.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 9560bf2a3b..07e4ddf844 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -449,7 +449,6 @@ let extend_constr state forpat ng =
let isforpat = target_to_bool forpat in
let needed_levels, state = register_empty_levels state isforpat pure_sublevels in
let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in
- let nb_decls = List.length needed_levels + 1 in
let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in
let empty = { constrs = []; constrlists = []; binders = [] } in
let act = ty_eval r (make_act forpat ng.notgram_notation) empty in