diff options
Diffstat (limited to 'pretyping/redops.ml')
| -rw-r--r-- | pretyping/redops.ml | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/pretyping/redops.ml b/pretyping/redops.ml index c188995a..7d65925e 100644 --- a/pretyping/redops.ml +++ b/pretyping/redops.ml @@ -14,25 +14,29 @@ let make_red_flag l = let rec add_flag red = function | [] -> red | FBeta :: lf -> add_flag { red with rBeta = true } lf - | FIota :: lf -> add_flag { red with rIota = true } lf + | FMatch :: lf -> add_flag { red with rMatch = true } lf + | FFix :: lf -> add_flag { red with rFix = true } lf + | FCofix :: lf -> add_flag { red with rCofix = true } lf | FZeta :: lf -> add_flag { red with rZeta = true } lf | FConst l :: lf -> if red.rDelta then - Errors.error + CErrors.error "Cannot set both constants to unfold and constants not to unfold"; add_flag { red with rConst = union_consts red.rConst l } lf | FDeltaBut l :: lf -> if red.rConst <> [] && not red.rDelta then - Errors.error + CErrors.error "Cannot set both constants to unfold and constants not to unfold"; add_flag { red with rConst = union_consts red.rConst l; rDelta = true } lf in add_flag - {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []} + {rBeta = false; rMatch = false; rFix = false; rCofix = false; + rZeta = false; rDelta = false; rConst = []} l let all_flags = - {rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []} + {rBeta = true; rMatch = true; rFix = true; rCofix = true; + rZeta = true; rDelta = true; rConst = []} |