diff options
| author | letouzey | 2013-10-23 22:17:07 +0000 |
|---|---|---|
| committer | letouzey | 2013-10-23 22:17:07 +0000 |
| commit | 5e6145c871eea1e94566b252b4bfc4cd752f42d5 (patch) | |
| tree | 97dfa98357cb0cf90bf06c9d470e6788de84c3b1 /pretyping/redops.ml | |
| parent | 9b56e832ef591379dd1f2b29fe7d88513f7caf50 (diff) | |
cList: set-as-list functions are now with an explicit comparison
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/redops.ml')
| -rw-r--r-- | pretyping/redops.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/pretyping/redops.ml b/pretyping/redops.ml index 1713a371ea..687cf6e467 100644 --- a/pretyping/redops.ml +++ b/pretyping/redops.ml @@ -8,6 +8,8 @@ open Genredexpr +let union_consts l1 l2 = Util.List.union Pervasives.(=) l1 l2 (* FIXME *) + let make_red_flag l = let rec add_flag red = function | [] -> red @@ -18,14 +20,14 @@ let make_red_flag l = if red.rDelta then Errors.error "Cannot set both constants to unfold and constants not to unfold"; - add_flag { red with rConst = Util.List.union red.rConst l } lf + add_flag { red with rConst = union_consts red.rConst l } lf | FDeltaBut l :: lf -> if red.rConst <> [] && not red.rDelta then Errors.error "Cannot set both constants to unfold and constants not to unfold"; add_flag - { red with rConst = Util.List.union red.rConst l; rDelta = true } - lf + { red with rConst = union_consts red.rConst l; rDelta = true } + lf in add_flag {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []} |