From 7817af48a554573fb649028263ecfc0fabe400d8 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 23 Jun 2018 15:08:55 +0200
Subject: Remove useless is_projection in tacred

---
 pretyping/tacred.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 40c4cfaa45..869d14c627 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -49,7 +49,7 @@ let error_not_evaluable r =
 
 let is_evaluable_const env cst =
   is_transparent env (ConstKey cst) && 
-    (evaluable_constant cst env || is_projection cst env)
+  evaluable_constant cst env
 
 let is_evaluable_var env id =
   is_transparent env (VarKey id) && evaluable_named id env
-- 
cgit v1.2.3