diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-04-01 17:35:39 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:45:19 +0200 |
| commit | fd1f420aef96822bed2ce14214c34e41ceda9b4e (patch) | |
| tree | 50a0e42a1a5a9ab9edc05f6c4a14a2f55df0cbf7 /printing/printer.mli | |
| parent | 4dd4f186895d16510f217778bb83933be8956082 (diff) | |
Using UInfoInd for universes in inductive types
It stores both universe constraints and subtyping information for
blocks of inductive declarations.
At this stage the there is no inference or checking implemented. The
subtyping information simply encodes equality of levels for the condition of
subtyping.
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/printing/printer.mli b/printing/printer.mli index 3fce06561..6531036a1 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -97,6 +97,7 @@ val pr_sort : evar_map -> sorts -> std_ppcmds val pr_polymorphic : bool -> std_ppcmds val pr_universe_instance : evar_map -> Univ.universe_context -> std_ppcmds val pr_universe_ctx : evar_map -> Univ.universe_context -> std_ppcmds +val pr_universe_info_ind : evar_map -> Univ.universe_info_ind -> std_ppcmds (** Printing global references using names as short as possible *) |