diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-06 22:48:32 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-05-03 13:37:56 +0200 |
| commit | e9b745af47ba3386724b874e3fd74b6dad33b015 (patch) | |
| tree | 2d6953e463d5d0dad13a29e4340b16671681a731 /pretyping/detyping.ml | |
| parent | 4bff930da2c029a66eaf5378e5abd2cc35554f8f (diff) | |
Allow flexible anonymous universes in instances and sorts.
The addition to the test suite showcases the usage.
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 7 |
1 files changed, 5 insertions, 2 deletions
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 |