diff options
| author | Pierre-Marie Pédrot | 2018-07-25 22:00:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-25 22:00:33 +0200 |
| commit | 535f8ce6edea2e2692f5c9c094d3c6fd07411897 (patch) | |
| tree | 8ce9fab779fe91e6a1fa12eba1718f9eda763efb /printing/printmod.ml | |
| parent | e1f7bb0bba093e5e5398bfe5a2a5d0ffabdf1405 (diff) | |
| parent | ca9e02ad1882cc4268ae1bcf0f573d24b92fa695 (diff) | |
Merge PR #7859: Remove himsg.pr_puniverses, use @{} for universe printing in errors
Diffstat (limited to 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index 3f95dcfb6d..e2d9850bf8 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -103,9 +103,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) = let envpar = push_rel_context params env in let inst = if Declareops.inductive_is_polymorphic mib then - let ctx = Declareops.inductive_polymorphic_context mib in - let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in - Printer.pr_universe_instance sigma ctx + Printer.pr_universe_instance sigma u else mt () in hov 0 ( |