diff options
| author | Amin Timany | 2017-04-01 17:35:39 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-06-16 04:45:19 +0200 |
| commit | fd1f420aef96822bed2ce14214c34e41ceda9b4e (patch) | |
| tree | 50a0e42a1a5a9ab9edc05f6c4a14a2f55df0cbf7 /printing/printer.ml | |
| 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.ml')
| -rw-r--r-- | printing/printer.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index d6f0778f75..c27a9b009d 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -261,6 +261,13 @@ let pr_universe_ctx sigma c = else mt() +let pr_universe_info_ind sigma uii = + if !Detyping.print_universes && not (Univ.UInfoInd.is_empty uii) then + fnl()++pr_in_comment (fun uii -> v 0 + (Univ.pr_universe_info_ind (Termops.pr_evd_level sigma) uii)) uii + else + mt() + (**********************************************************************) (* Global references *) |