diff options
Diffstat (limited to 'proofs/redexpr.ml')
| -rw-r--r-- | proofs/redexpr.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index ee5591521..55dfb88b4 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -146,7 +146,10 @@ let make_flag_constant = function let make_flag env f = let red = no_red in let red = if f.rBeta then red_add red fBETA else red in - let red = if f.rIota then red_add red fIOTA else red in + let red = + if f.rIota then (red_add (red_add (red_add red fMATCH) fFIX) fCOFIX) + else red + in let red = if f.rZeta then red_add red fZETA else red in let red = if f.rDelta then (* All but rConst *) |