From 5bca0e81c46c1cc6427f939263670996f570dbcf Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 2 Feb 2016 15:47:23 +0100
Subject: Fix part of bug #4533: respect declared global transparency of
 projections in unification.ml

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

(limited to 'pretyping')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 6cb1bc7028..55210d067e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -481,7 +481,8 @@ let key_of env b flags f =
       Id.Pred.mem id (fst flags.modulo_delta) ->
     Some (IsKey (VarKey id))
   | Proj (p, c) when Projection.unfolded p
-      || Cpred.mem (Projection.constant p) (snd flags.modulo_delta) ->
+    || (is_transparent env (ConstKey (Projection.constant p)) &&
+       (Cpred.mem (Projection.constant p) (snd flags.modulo_delta))) ->
     Some (IsProj (p, c))
   | _ -> None
   
-- 
cgit v1.2.3