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 /vernac | |
| 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 '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 |