diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-27 13:28:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-27 13:28:44 +0200 |
| commit | 04e0f9fde8789a28b66f24000ac8c831ff0815af (patch) | |
| tree | b9e3d026e192e7b5b0409594b11fb95ed138b6cb /kernel/term.ml | |
| parent | d9e6bed640083fce067343f24183382cc8e6ca7b (diff) | |
| parent | 8d89102e84d41956fb1359089d573cc64d7838ca (diff) | |
Merge PR #7863: Remove Sorts.contents
Diffstat (limited to 'kernel/term.ml')
| -rw-r--r-- | kernel/term.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index b44e038e9..81e344e73 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -16,14 +16,11 @@ open Vars open Constr (* Deprecated *) -type contents = Sorts.contents = Pos | Null -[@@ocaml.deprecated "Alias for Sorts.contents"] - type sorts_family = Sorts.family = InProp | InSet | InType [@@ocaml.deprecated "Alias for Sorts.family"] type sorts = Sorts.t = - | Prop of Sorts.contents (** Prop and Set *) + | Prop | Set | Type of Univ.Universe.t (** Type *) [@@ocaml.deprecated "Alias for Sorts.t"] |