diff options
Diffstat (limited to 'pretyping/glob_term.ml')
| -rw-r--r-- | pretyping/glob_term.ml | 22 |
1 files changed, 20 insertions, 2 deletions
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 84be15552..6ecb479e6 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -17,12 +17,30 @@ arguments and pattern-matching compilation are not. *) open Names -open Globnames open Decl_kinds open Misctypes type existential_name = Id.t +(** Sorts *) + +type 'a glob_sort_gen = + | GProp (** representation of [Prop] literal *) + | GSet (** representation of [Set] literal *) + | GType of 'a (** representation of [Type] literal *) + +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 + (** The kind of patterns that occurs in "match ... with ... end" locs here refers to the ident's location, not whole pat *) @@ -36,7 +54,7 @@ type cases_pattern = [ `any ] cases_pattern_g (** Representation of an internalized (or in other words globalized) term. *) type 'a glob_constr_r = - | GRef of global_reference * glob_level list option + | GRef of GlobRef.t * glob_level list option (** An identifier that represents a reference to an object defined either in the (global) environment or in the (local) context. *) | GVar of Id.t |