diff options
| author | Hugo Herbelin | 2018-11-14 10:10:39 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-06-01 18:00:39 +0200 |
| commit | 460bf801123d13e8c82503a2fc491892f8eed6d5 (patch) | |
| tree | 1abb0e786b727e5947ab2a5e5708d02a712a8593 /parsing/pcoq.mli | |
| parent | 45352e43db4c67eab23517f13e94ba1b5cc11808 (diff) | |
Allowing Set to be part of universe expressions.
Conversely, Type existential variables now (explicitly) cover the Set
case.
Similarly for Prop and SProp.
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 |