diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/printers.mllib | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index 07b48ed573..f19edf1c80 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -55,6 +55,7 @@ Monad Names Univ +UGraph Esubst Uint31 Sorts diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 0900bb0962..1d3d711ac7 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -221,7 +221,7 @@ let ppuniverseconstraints c = pp (Universes.Constraints.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx -let ppuniverses u = pp (Univ.pr_universes Level.pr u) +let ppuniverses u = pp (UGraph.pr_universes Level.pr u) let ppnamedcontextval e = pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e)) |