diff options
| author | Emilio Jesus Gallego Arias | 2020-06-30 12:55:02 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-30 12:55:02 +0200 |
| commit | bffe3e8dcbb6019b30d32081f0b56eba30bf8be7 (patch) | |
| tree | b2884dfed06b740e2b4fd44ff7cec61ca716f906 /printing/printmod.ml | |
| parent | c2b76962b407cac8de4465be1e77cf45ff5822d9 (diff) | |
| parent | ae1acfefe52937ea7e3a098137df032363051361 (diff) | |
Merge PR #11977: Generate default names for bound universes of polymorphic definitions
Reviewed-by: ejgallego
Reviewed-by: herbelin
Diffstat (limited to 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index eec2fe86ac..9beac17546 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -118,7 +118,7 @@ let print_mutual_inductive env mind mib udecl = | BiFinite -> "Variant" | CoFinite -> "CoInductive" in - let bl = UnivNames.universe_binders_with_opt_names + let bl = Printer.universe_binders_with_opt_names (Declareops.inductive_polymorphic_context mib) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in @@ -151,7 +151,7 @@ let print_record env mind mib udecl = let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in let fields = get_fields cstrtype in let envpar = push_rel_context params env in - let bl = UnivNames.universe_binders_with_opt_names (Declareops.inductive_polymorphic_context mib) + let bl = Printer.universe_binders_with_opt_names (Declareops.inductive_polymorphic_context mib) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in @@ -290,7 +290,7 @@ let print_body is_impl extent env mp (l,body) = (match extent with | OnlyNames -> mt () | WithContents -> - let bl = UnivNames.universe_binders_with_opt_names ctx None in + let bl = Printer.universe_binders_with_opt_names ctx None in let sigma = Evd.from_ctx (UState.of_binders bl) in str " :" ++ spc () ++ hov 0 (Printer.pr_ltype_env env sigma cb.const_type) ++ |