From 7f427a8ab2e08e24c303cffd2e54d4fb477f3b00 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 12 Feb 2015 15:40:10 +0100
Subject: Fixing #3997 (occur-check in the presence of primitive projections,
 patch from Matthieu).

---
 pretyping/evarsolve.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 5aa72c90ac..921609aae3 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -186,6 +186,7 @@ let noccur_evar env evd evk c =
       (match pi2 (Environ.lookup_rel (i-k) env) with
        | None -> ()
        | Some b -> occur_rec k (lift i b))
+  | Proj (p,c) -> occur_rec k (Retyping.expand_projection env evd p c [])
   | _ -> iter_constr_with_binders succ occur_rec k c
   in
   try occur_rec 0 c; true with Occur -> false
-- 
cgit v1.2.3