aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/pcoq.ml4')
-rw-r--r--parsing/pcoq.ml41
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 73e0b4cc8..cc7bb3dad 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -323,6 +323,7 @@ module Prim =
let base_ident = Gram.Entry.create "Prim.base_ident"
let qualid = Gram.Entry.create "Prim.qualid"
+ let fullyqualid = Gram.Entry.create "Prim.fullyqualid"
let dirpath = Gram.Entry.create "Prim.dirpath"
let ne_string = Gram.Entry.create "Prim.ne_string"