diff options
| author | Pierre-Marie Pédrot | 2016-10-08 17:14:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-10-08 17:14:38 +0200 |
| commit | 82eb6cbfa3db53756ea40fb4795836d6f8c55bbe (patch) | |
| tree | 2721409ee43e729c82d5e3337d58bbbdb3f461aa /pretyping/evarconv.ml | |
| parent | 8110e9cbd6d70960a221c316774460f6ad6dc5e9 (diff) | |
| parent | 0a6f0c161756a1878dd81e438df86f08631d8399 (diff) | |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'pretyping/evarconv.ml')
| -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 b033f5a395..b7e0535dad 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -42,12 +42,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 = |