diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2017-12-01 10:11:41 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2017-12-01 10:16:49 +0100 |
| commit | 20c98eab851210702b39e1c66e005acfc351d8dd (patch) | |
| tree | 957aab7aadfda8c10f251ff9d83f3f5b05c07dc5 /intf | |
| parent | 0048cbe810c82a775558c14cd7fcae644e205c51 (diff) | |
Proper nametab handling of global universe names
They are now bound at the library + module level and can be qualified
and shadowed according to the usual rules of qualified names.
Parsing and printing of universes "u+n" done as well.
In sections, global universes are discharged as well, checking that
they can be defined globally when they are introduced
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/misctypes.ml | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/intf/misctypes.ml b/intf/misctypes.ml index 87484ccd5..33e961419 100644 --- a/intf/misctypes.ml +++ b/intf/misctypes.ml @@ -48,13 +48,19 @@ 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 = Name.t Loc.located list -type level_info = Name.t Loc.located option -type glob_sort = sort_info glob_sort_gen +type 'a universe_kind = + | UAnonymous + | UUnknown + | UNamed of 'a + +type level_info = Libnames.reference universe_kind type glob_level = level_info glob_sort_gen type glob_constraint = glob_level * Univ.constraint_type * glob_level +type sort_info = (Libnames.reference * int) option list +type glob_sort = sort_info glob_sort_gen + (** A synonym of [Evar.t], also defined in Term *) type existential_key = Evar.t |