diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 5f982346ab..196835f184 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -182,6 +182,7 @@ module Constr : val operconstr : constr_expr Entry.t val ident : Id.t Entry.t val global : qualid Entry.t + val universe_name : Glob_term.glob_sort_name Entry.t val universe_level : Glob_term.glob_level Entry.t val sort : Glob_term.glob_sort Entry.t val sort_family : Sorts.family Entry.t |