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 /pretyping | |
| 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 '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 |