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. --- intf/misctypes.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'intf') diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 33dc2a335..7c2dc5177 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -48,8 +48,8 @@ type 'a glob_sort_gen = | GProp (** representation of [Prop] literal *) | GSet (** representation of [Set] literal *) | GType of 'a (** representation of [Type] literal *) -type sort_info = string Loc.located list -type level_info = string Loc.located option +type sort_info = Name.t Loc.located list +type level_info = Name.t Loc.located option type glob_sort = sort_info glob_sort_gen type glob_level = level_info glob_sort_gen -- cgit v1.2.3