diff options
| author | Pierre-Marie Pédrot | 2020-01-17 13:40:10 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-02 19:30:04 +0100 |
| commit | 238b0cb82a1e66332131f10de79f4abe55d4b0b2 (patch) | |
| tree | 583532caeb28c940c01766f8a7578a90e7a55b0b /engine/evd.ml | |
| parent | 47c1730d4a7c02ba56d0292143f25772319dd98c (diff) | |
Move kind_of_type from the kernel to ssr.
It was virtually unused except in ssr, and there is no reason to clutter
the kernel with irrelevant code.
Fixes #9390: What is the purpose of the function "kind_of_type"?
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 70f58163fd..4bfa7c45e3 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1364,7 +1364,6 @@ module MiniEConstr = struct let kind sigma c = Constr.kind (whd_evar sigma c) let kind_upto = kind - let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c) let of_kind = Constr.of_kind let of_constr c = c let of_constr_array v = v |