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/himsg.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 'vernac/himsg.ml')
| -rw-r--r-- | vernac/himsg.ml | 2 |
1 files changed, 1 insertions, 1 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 |