From 1b09098cc4830f262820d2935a9cd0afa383ed3f Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 1 Jul 2016 13:57:14 +0200 Subject: Add and document match, fix and cofix reduction flags. --- pretyping/redops.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'pretyping') diff --git a/pretyping/redops.ml b/pretyping/redops.ml index c188995a8..db5879174 100644 --- a/pretyping/redops.ml +++ b/pretyping/redops.ml @@ -14,7 +14,9 @@ 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 @@ -30,9 +32,11 @@ let make_red_flag l = 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 = []} -- cgit v1.2.3