From 1be6169d6402d074664f805b3ee8f6fd543d3724 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 11 Dec 2018 10:43:52 +0100
Subject: [arguments] cleanup

---
 pretyping/arguments_renaming.ml | 28 ++++++++++++++++------------
 1 file 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 =
-- 
cgit v1.2.3