aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZRange.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-04-01 22:39:58 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2017-04-02 02:05:58 -0400
commitd5006369495a4e79c4db011d8fdb334b266381f2 (patch)
tree22c4c7079435df4dea10fcd6ca86e5a0da72f59c /src/Util/ZRange.v
parent92f7ffd5e4f6db8529e41d0659b1b69218dac779 (diff)
Coalesce Tuple.pointwise2 and Tuple.fieldwise
We don't need both of them. We keep the definition of pointwise2 because it's needed for reification to work, and we keep the name of fieldwise because it's used in more places. This closes #137.
Diffstat (limited to 'src/Util/ZRange.v')
-rw-r--r--src/Util/ZRange.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ZRange.v b/src/Util/ZRange.v
index fab098037..2c286aa9e 100644
--- a/src/Util/ZRange.v
+++ b/src/Util/ZRange.v
@@ -34,7 +34,7 @@ Section with_bitwidth.
end.
Definition is_bounded_by {n} : Tuple.tuple zrange n -> Tuple.tuple Z n -> Prop
- := Tuple.pointwise2 is_bounded_by'.
+ := Tuple.fieldwise is_bounded_by'.
End with_bitwidth.
Definition is_tighter_than_bool (x y : zrange) : bool