diff options
| -rw-r--r-- | pretyping/arguments_renaming.ml | 28 |
1 files changed, 16 insertions, 12 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 3da1ab7439..0ace11839e 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -69,19 +69,23 @@ let rename_arguments local r names = let arguments_names r = GlobRef.Map.find r !name_table -let rec rename_prod c = function - | [] -> c - | (Name _ as n) :: tl -> - (match kind_of_type c with - | ProdType (_, s, t) -> mkProd (n, s, rename_prod t tl) - | _ -> c) - | _ :: tl -> - match kind_of_type c with - | ProdType (n, s, t) -> mkProd (n, s, rename_prod t tl) - | _ -> c - let rename_type ty ref = - try rename_prod ty (arguments_names ref) + let name_override old_name override = + match override with + | Name _ as x -> x + | Anonymous -> old_name in + let rec rename_type_aux c = function + | [] -> c + | rename :: rest as renamings -> + match kind_of_type c with + | ProdType (old, s, t) -> + mkProd (name_override old rename, s, rename_type_aux t rest) + | LetInType(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 + try rename_type_aux ty (arguments_names ref) with Not_found -> ty let rename_type_of_constant env c = |