aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/pcoq.ml')
-rw-r--r--parsing/pcoq.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 0525ffb77..cf65262c4 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -287,6 +287,7 @@ module Prim =
let name = Gram.entry_create "Prim.name"
let identref = Gram.entry_create "Prim.identref"
+ let pidentref = Gram.entry_create "Prim.pidentref"
let pattern_ident = Gram.entry_create "pattern_ident"
let pattern_identref = Gram.entry_create "pattern_identref"