diff options
Diffstat (limited to 'intf/misctypes.mli')
| -rw-r--r-- | intf/misctypes.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 2aec5ed32..a51145812 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -37,7 +37,8 @@ type 'id move_location = (** Sorts *) -type glob_sort = GProp | GSet | GType of Univ.universe option +type sort_info = Pp.std_ppcmds option +type glob_sort = GProp | GSet | GType of sort_info (** Casts *) |