diff options
| author | Maxime Dénès | 2017-11-13 17:13:44 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-13 17:13:44 +0100 |
| commit | 8d176db01baf9fb4a5e07decb9500ef4a8717e93 (patch) | |
| tree | 675b02e411ff2c56a9aff39f4956a055eac254a7 /kernel/sorts.ml | |
| parent | 29a7307ea7cd36408661ba633a235793f11dca84 (diff) | |
| parent | 03e21974a3e971a294533bffb81877dc1bd270b6 (diff) | |
Merge PR #6098: [api] Move structures deprecated in the API to the core.
Diffstat (limited to 'kernel/sorts.ml')
| -rw-r--r-- | kernel/sorts.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/sorts.ml b/kernel/sorts.ml index cf5207e8dc..07688840dd 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -14,7 +14,7 @@ type family = InProp | InSet | InType type t = | Prop of contents (* proposition types *) - | Type of universe + | Type of Universe.t let prop = Prop Null let set = Prop Pos @@ -91,7 +91,7 @@ module Hsorts = struct type _t = t type t = _t - type u = universe -> universe + type u = Universe.t -> Universe.t let hashcons huniv = function | Type u as c -> |