diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-16 15:22:49 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-18 15:58:09 +0100 |
| commit | e4423ce78823ad9dd8c726e31de712e67a91893a (patch) | |
| tree | 62e5a808b873ab432341b7b77797f9a2312f1092 | |
| parent | 7a373e3853256b518d8ccb69fa6282211d500e0c (diff) | |
COMMENTS: added to some variants of "Misctypes.glob_sort_gen" type.
| -rw-r--r-- | intf/misctypes.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 5c11119ed..65c7dccf2 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -43,7 +43,10 @@ type 'id move_location = (** Sorts *) -type 'a glob_sort_gen = GProp | GSet | GType of 'a +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 |