diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 70c5ceded..9254a6ff8 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -21,9 +21,9 @@ type sorts = | Prop of contents (* Prop and Set *) | Type of Univ.universe (* Type *) -val mk_Set : sorts -val mk_Prop : sorts -val type_0 : sorts +val set_sort : sorts +val prop_sort : sorts +val type1_sort : sorts (*s The sorts family of CCI. *) |