From d5006369495a4e79c4db011d8fdb334b266381f2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 1 Apr 2017 22:39:58 -0400 Subject: 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. --- src/Util/ZRange.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Util/ZRange.v') 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 -- cgit v1.2.3