diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-10-06 11:38:06 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-10-06 11:38:06 +0200 |
| commit | 0a6f0c161756a1878dd81e438df86f08631d8399 (patch) | |
| tree | ab35fbeda0f95af2e9ade4fa153c5155b118e505 /pretyping | |
| parent | 08f4cfc9dfb03973ae652ef6576342ae38f8f199 (diff) | |
evarconv.ml: Fix bug #4529, primproj unfolding
Evarconv was made precociously dependent on user-declared reduction
behaviors. Only cbn should rely on that.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index aead1cb35..0d261f7f8 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 = |