From b0ef649660542ae840ea945d7ab4f1f3ae7b85cd Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 28 Apr 2018 17:58:08 +0200 Subject: Split off Universes functions dealing with names. This API is a bit strange, I expect it will change at some point. --- engine/termops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine/termops.ml') diff --git a/engine/termops.ml b/engine/termops.ml index df43be28e..9e975da58 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -47,7 +47,7 @@ let pr_fix pr_constr ((t,i),(lna,tl,bl)) = let pr_puniverses p u = if Univ.Instance.is_empty u then p - else p ++ str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)" + else p ++ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)" let rec pr_constr c = match kind c with | Rel n -> str "#"++int n -- cgit v1.2.3