aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/egramcoq.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/egramcoq.ml')
-rw-r--r--parsing/egramcoq.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 1b38a013c..870137ca1 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -443,7 +443,7 @@ let make_act : type r. r target -> _ -> r gen_eval = function
CAst.make ~loc @@ CPatNotation (notation, env, [])
let extend_constr state forpat ng =
- let n = ng.notgram_level in
+ let n,_,_ = ng.notgram_level in
let assoc = ng.notgram_assoc in
let (entry, level) = interp_constr_entry_key forpat n in
let fold (accu, state) pt =