diff options
| author | Gaëtan Gilbert | 2020-03-31 15:10:32 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-06-25 14:17:21 +0200 |
| commit | ae1acfefe52937ea7e3a098137df032363051361 (patch) | |
| tree | e9286129872296964cce1b59ab6171c4afb6647d /printing/printmod.ml | |
| parent | 50361dc784c8967e7c4b254102e2cb21cb7e9f9e (diff) | |
Generate names for anonymous polymorphic universes
This should make the univbinders output test less fragile as it
depends less on the global counter (still used for universes from
section variables).
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) ++ |