diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index df9084ab76..8bff5cfd94 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -187,9 +187,9 @@ module Constr : [@@deprecated "Deprecated in 8.13; use 'term' instead"] 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 universe_name : sort_name_expr Entry.t + val universe_level : univ_level_expr Entry.t + val sort : sort_expr Entry.t val sort_family : Sorts.family Entry.t val pattern : cases_pattern_expr Entry.t val constr_pattern : constr_expr Entry.t |