diff options
| author | Matthieu Sozeau | 2014-09-08 10:23:12 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-08 17:09:43 +0200 |
| commit | 26a79004e47bbdc97df61015ce7e944eef14ac71 (patch) | |
| tree | 1f24c9acbb73cd63dcc689222b965f245767137e /intf | |
| parent | 89ad50f4d7e1312539995ced3a632821bf6af7c5 (diff) | |
Parsing of Type@{max(i,j)}.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.mli | 2 | ||||
| -rw-r--r-- | intf/glob_term.mli | 2 | ||||
| -rw-r--r-- | intf/misctypes.mli | 8 |
3 files changed, 8 insertions, 4 deletions
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index c28c4dcb18..eb39a9bde6 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -61,7 +61,7 @@ and cases_pattern_notation_substitution = cases_pattern_expr list * (** for constr subterms *) cases_pattern_expr list list (** for recursive notations *) -type instance_expr = Misctypes.glob_sort list +type instance_expr = Misctypes.glob_level list type constr_expr = | CRef of reference * instance_expr option diff --git a/intf/glob_term.mli b/intf/glob_term.mli index b4543bb59b..d0b6939e24 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -28,7 +28,7 @@ type cases_pattern = (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *) type glob_constr = - | GRef of (Loc.t * global_reference * glob_sort list option) + | GRef of (Loc.t * global_reference * glob_level list option) | GVar of (Loc.t * Id.t) | GEvar of Loc.t * existential_key * glob_constr list option | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *) diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 390711fabd..c61da0e306 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -43,8 +43,12 @@ type 'id move_location = (** Sorts *) -type sort_info = string option -type glob_sort = GProp | GSet | GType of sort_info +type 'a glob_sort_gen = GProp | GSet | GType of 'a +type sort_info = string list +type level_info = string option + +type glob_sort = sort_info glob_sort_gen +type glob_level = level_info glob_sort_gen (** A synonym of [Evar.t], also defined in Term *) |