From 1bf30962d7cd5732393d7722ae6d263d4c812ec8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 9 Jul 2015 10:32:17 +0200
Subject: Make retyping of projections more resilient to wrong environment.

Unfortunately, it seems that retyping can be called in ill-typed terms and/or in
the wrong environment. This was broken for projections by my commit
a51cce369b9c634a93120092d4c7685a242d55b1
---
 pretyping/retyping.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 743bc3b19b..fb55265526 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -126,9 +126,11 @@ let retype ?(polyprop=true) sigma =
     | App(f,args) ->
         strip_outer_cast
           (subst_type env sigma (type_of env f) (Array.to_list args))
-    | Proj (p,c) -> 
+    | Proj (p,c) ->
        let ty = type_of env c in
-       Inductiveops.type_of_projection_knowing_arg env sigma p c ty
+       (try
+	   Inductiveops.type_of_projection_knowing_arg env sigma p c ty
+	 with Invalid_argument _ -> retype_error BadRecursiveType)
     | Cast (c,_, t) -> t
     | Sort _ | Prod _ -> mkSort (sort_of env cstr)
 
-- 
cgit v1.2.3