From 0a6f0c161756a1878dd81e438df86f08631d8399 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 6 Oct 2016 11:38:06 +0200
Subject: evarconv.ml: Fix bug #4529, primproj unfolding

Evarconv was made precociously dependent on user-declared reduction
behaviors. Only cbn should rely on that.
---
 pretyping/evarconv.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'pretyping/evarconv.ml')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index aead1cb35f..0d261f7f87 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -39,12 +39,7 @@ let _ = Goptions.declare_bool_option {
 let unfold_projection env evd ts p c =
   let cst = Projection.constant p in
     if is_transparent_constant ts cst then
-      let c' = Some (mkProj (Projection.make cst true, c)) in
-	match ReductionBehaviour.get (Globnames.ConstRef cst) with
-	| None -> c'
-	| Some (recargs, nargs, flags) ->
-	  if (List.mem `ReductionNeverUnfold flags) then None
-	  else c'
+      Some (mkProj (Projection.make cst true, c))
     else None
       
 let eval_flexible_term ts env evd c =
-- 
cgit v1.2.3