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 /vernac | |
| 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 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 2 | ||||
| -rw-r--r-- | vernac/prettyp.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 9d67ce3757..540d470fdc 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -957,7 +957,7 @@ let explain_not_match_error = function let pr_auctx auctx = let sigma = Evd.from_ctx (UState.of_binders - (UnivNames.universe_binders_with_opt_names auctx None)) + (Printer.universe_binders_with_opt_names auctx None)) in let uctx = AUContext.repr auctx in Printer.pr_universe_instance_constraints sigma diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index faf53d3fad..80e0b9987f 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -75,7 +75,7 @@ let print_ref reduce ref udecl = let env = Global.env () in let typ, univs = Typeops.type_of_global_in_context env ref in let inst = Univ.make_abstract_instance univs in - let bl = UnivNames.universe_binders_with_opt_names (Environ.universes_of_global env ref) udecl in + let bl = Printer.universe_binders_with_opt_names (Environ.universes_of_global env ref) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in let typ = EConstr.of_constr typ in let typ = @@ -633,7 +633,7 @@ let print_constant with_values sep sp udecl = in let ctx = UState.of_binders - (UnivNames.universe_binders_with_opt_names (Declareops.constant_polymorphic_context cb) udecl) + (Printer.universe_binders_with_opt_names (Declareops.constant_polymorphic_context cb) udecl) in let env = Global.env () and sigma = Evd.from_ctx ctx in let pr_ltype = pr_ltype_env env sigma in |