From e9b745af47ba3386724b874e3fd74b6dad33b015 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Thu, 6 Apr 2017 22:48:32 +0200 Subject: Allow flexible anonymous universes in instances and sorts. The addition to the test suite showcases the usage. --- pretyping/detyping.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'pretyping/detyping.ml') diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 483e2b432..8a90a3f9b 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -422,7 +422,9 @@ let detype_sort sigma = function | Type u -> GType (if !print_universes - then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u)] + then + let u = Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u) in + [dl, Name.mk_name (Id.of_string_soft u)] else []) type binder_kind = BProd | BLambda | BLetIn @@ -434,7 +436,8 @@ let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index let set_detype_anonymous f = detype_anonymous := f let detype_level sigma l = - GType (Some (dl, Pp.string_of_ppcmds (Termops.pr_evd_level sigma l))) + let l = Pp.string_of_ppcmds (Termops.pr_evd_level sigma l) in + GType (Some (dl, Name.mk_name (Id.of_string_soft l))) let detype_instance sigma l = let l = EInstance.kind sigma l in -- cgit v1.2.3