From 9f09cbfe36c38a97644ea98c5497636fe74d98d6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 27 Feb 2015 18:59:59 +0100
Subject: Taking current env and not global env in b286c9f4f42f (4 commits ago,
 as revealed by #2141).

---
 pretyping/retyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 213d7ddda4..a56861c683 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -109,7 +109,7 @@ let retype ?(polyprop=true) sigma =
             Inductiveops.find_rectype env sigma t
           with Not_found -> retype_error BadRecursiveType
         in
-        let n = inductive_nrealdecls (fst (fst (dest_ind_family indf))) in
+        let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in
         let t = betazetaevar_applist sigma n p realargs in
         (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with
           | Prod _ -> whd_beta sigma (applist (t, [c]))
-- 
cgit v1.2.3