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 /engine/evd.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 '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 |