From df5e18302e113370906d9ca0b2a2e96dcaccbf0a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 14 Feb 2014 14:19:53 +0100
Subject: Honor the Opaque flag for projections in simpl.

---
 pretyping/tacred.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 383d233069..1ba6350b5c 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -728,12 +728,14 @@ and whd_simpl_stack env sigma =
 
       | Proj (p, c) ->
         (try 
- 	   (match recargs (EvalConst p) with
- 	   | Some (_, n) when n > 1 -> (* simpl never *) s'
- 	   | _ ->
-	     match reduce_projection env sigma p (whd_construct_stack env sigma c) stack with
-	     | Reduced s' -> redrec (applist s')
-	     | NotReducible -> s')
+	   if is_evaluable env (EvalConstRef p) then
+ 	     (match recargs (EvalConst p) with
+ 	     | Some (_, n) when n > 1 -> (* simpl never *) s'
+ 	     | _ ->
+	       match reduce_projection env sigma p (whd_construct_stack env sigma c) stack with
+	       | Reduced s' -> redrec (applist s')
+	       | NotReducible -> s')
+	   else s'
 	 with Redelimination -> s')
 	  
       | _ -> 
-- 
cgit v1.2.3