From d335953af623429092303076c7bcf06ee5de50db Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 1 Oct 2014 16:06:29 +0200
Subject: Fixing use of arguments renaming in apply which was broken after
 reorganization of apply in d5fece25d8964d5d9fcd55b66164286aeef5fb9f: using
 renaming also in retyping.

---
 dev/printers.mllib        | 2 +-
 pretyping/pretyping.mllib | 2 +-
 pretyping/retyping.ml     | 7 ++++---
 3 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 1d09ce105e..a655bc5266 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -120,6 +120,7 @@ Glob_ops
 Redops
 Reductionops
 Inductiveops
+Arguments_renaming
 Nativenorm
 Retyping
 Cbv
@@ -128,7 +129,6 @@ Evarutil
 Evarsolve
 Recordops
 Evarconv
-Arguments_renaming
 Typing
 Patternops
 ConstrMatching
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index a00fec30e8..b189360c07 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -5,6 +5,7 @@ Evd
 Reductionops
 Vnorm
 Inductiveops
+Arguments_renaming
 Nativenorm
 Retyping
 Cbv
@@ -14,7 +15,6 @@ Evarutil
 Evarsolve
 Recordops
 Evarconv
-Arguments_renaming
 Typing
 Miscops
 Glob_ops
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 89ad9ee683..23ad43a1c3 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -17,6 +17,7 @@ open Names
 open Reductionops
 open Environ
 open Termops
+open Arguments_renaming
 
 type retype_error =
   | NotASort
@@ -94,10 +95,10 @@ let retype ?(polyprop=true) sigma =
         let (_,_,ty) = lookup_rel n env in
         lift n ty
     | Var id -> type_of_var env id
-    | Const cst -> Typeops.type_of_constant_in env cst
+    | Const cst -> rename_type_of_constant env cst
     | Evar ev -> Evd.existential_type sigma ev
-    | Ind ind -> type_of_inductive env ind
-    | Construct cstr -> type_of_constructor env cstr
+    | Ind ind -> rename_type_of_inductive env ind
+    | Construct cstr -> rename_type_of_constructor env cstr
     | Case (_,p,c,lf) ->
         let Inductiveops.IndType(_,realargs) =
           let t = type_of env c in
-- 
cgit v1.2.3