From ac62cda8a4f488b94033b108c37556877232137a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 3 Mar 2015 09:41:51 +0100
Subject: Fix bug #4101, noccur_evar's expand_projection can legitimately fail
 when called from w_unify, so we protect it.

---
 pretyping/evarsolve.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 99d83a0e88..bfd19c6c7d 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -192,7 +192,13 @@ let noccur_evar env evd evk c =
       (match pi2 (Environ.lookup_rel i env) with
        | None -> ()
        | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b))
-  | Proj (p,c) -> occur_rec acc (Retyping.expand_projection env evd p c [])
+  | Proj (p,c) -> 
+    let c = 
+      try Retyping.expand_projection env evd p c []
+      with Retyping.RetypeError _ -> 
+	(* Can happen when called from w_unify which doesn't assign evars/metas 
+	   eagerly enough *) c
+    in occur_rec acc c
   | _ -> iter_constr_with_full_binders (fun rd (k,env) -> (succ k, push_rel rd env))
     occur_rec acc c
   in
-- 
cgit v1.2.3