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 /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/arguments_renaming.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 36f35a67c3..59ca418a39 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -11,7 +11,6 @@ (*i*) open Names open Globnames -open Term open Constr open Context open Environ @@ -78,14 +77,14 @@ let rename_type ty ref = let rec rename_type_aux c = function | [] -> c | rename :: rest as renamings -> - match kind_of_type c with - | ProdType (old, s, t) -> + match Constr.kind c with + | Prod (old, s, t) -> mkProd (name_override old rename, s, rename_type_aux t rest) - | LetInType(old, s, b, t) -> + | LetIn (old, s, b, t) -> mkLetIn (old ,s, b, rename_type_aux t renamings) - | CastType (t,_) -> rename_type_aux t renamings - | SortType _ -> c - | AtomicType _ -> c in + | Cast (t,_, _) -> rename_type_aux t renamings + | _ -> c + in try rename_type_aux ty (arguments_names ref) with Not_found -> ty |