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 ef707790c..9787af826 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -304,6 +304,7 @@ module Constr =
let binder_constr = gec_constr "binder_constr"
let ident = make_gen_entry uconstr "ident"
let global = make_gen_entry uconstr "global"
+ let universe_level = make_gen_entry uconstr "universe_level"
let sort = make_gen_entry uconstr "sort"
let pattern = Gram.entry_create "constr:pattern"
let constr_pattern = gec_constr "constr_pattern"