diff options
| author | Enrico Tassi | 2020-02-13 17:24:57 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-02-13 17:24:57 +0100 |
| commit | 6e020b001ec8b9d84293c5e9e7115bb1ddf901ca (patch) | |
| tree | 987e80de2abda3cb2b898e05d39db07d320c5edb /kernel/term.ml | |
| parent | eb83c142eb33de18e3bfdd7c32ecfb797a640c38 (diff) | |
| parent | b468bb9e7110be4e1a1c9b13da16720b64d1125e (diff) | |
Merge PR #11417: Move kind_of_type from the kernel to EConstr.
Reviewed-by: SkySkimmer
Reviewed-by: gares
Diffstat (limited to 'kernel/term.ml')
| -rw-r--r-- | kernel/term.ml | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 87678b911e..a2586e74f7 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -363,24 +363,3 @@ let rec isArity c = | Cast (c,_,_) -> isArity c | Sort _ -> true | _ -> false - -(** Kind of type *) - -(* Experimental, used in Presburger contrib *) -type ('constr, 'types) kind_of_type = - | SortType of Sorts.t - | CastType of 'types * 'types - | ProdType of Name.t Context.binder_annot * 'types * 'types - | LetInType of Name.t Context.binder_annot * 'constr * 'types * 'types - | AtomicType of 'constr * 'constr array - -let kind_of_type t = match kind t with - | Sort s -> SortType s - | Cast (c,_,t) -> CastType (c, t) - | Prod (na,t,c) -> ProdType (na, t, c) - | LetIn (na,b,t,c) -> LetInType (na, b, t, c) - | App (c,l) -> AtomicType (c, l) - | (Rel _ | Meta _ | Var _ | Evar _ | Const _ - | Proj _ | Case _ | Fix _ | CoFix _ | Ind _) - -> AtomicType (t,[||]) - | (Lambda _ | Construct _ | Int _ | Float _) -> failwith "Not a type" |