From df3d820b45695e273515f8d7cf7c0345c7d574c5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 17 Feb 2015 16:28:48 +0100
Subject: Fixing bug #4053.

---
 library/assumptions.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/library/assumptions.ml b/library/assumptions.ml
index 04ee14fb53..ab07b3647e 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -205,7 +205,8 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) =
 	| Fix (_,(_, e1_array, e2_array)) | CoFix (_,(_,e1_array, e2_array)) ->
           (iter_array e1_array) ** (iter_array e2_array)
 	| Const (kn,_) -> do_memoize_kn kn
-	| _ -> identity2 (* closed atomic types + rel *)
+	| Proj (_, e) -> iter e
+	| Rel _ | Sort _ | Ind _ | Construct _ -> identity2
     and iter_array a = Array.fold_right (fun e f -> (iter e)**f) a identity2
     in iter t s acc
 
-- 
cgit v1.2.3