diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 10f51b7acb..4b9b5fdcce 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -215,17 +215,6 @@ type ('constr, 'types) kind_of_term = term *) val kind_of_term : constr -> (constr, types) kind_of_term -val kind_of_term2 : constr -> ((constr,types) kind_of_term,constr) kind_of_term - -(** Experimental *) -type ('constr, 'types) kind_of_type = - | SortType of sorts - | CastType of 'types * 'types - | ProdType of name * 'types * 'types - | LetInType of name * 'constr * 'types * 'types - | AtomicType of 'constr * 'constr array - -val kind_of_type : types -> (constr, types) kind_of_type (** {6 Simple term case analysis. } *) |