aboutsummaryrefslogtreecommitdiff
path: root/src/Util/NUtil.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/NUtil.v')
-rw-r--r--src/Util/NUtil.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/NUtil.v b/src/Util/NUtil.v
index 1faa1da95..d76be63aa 100644
--- a/src/Util/NUtil.v
+++ b/src/Util/NUtil.v
@@ -117,7 +117,7 @@ Module N.
replace (Z.of_nat 2) with 2%Z by reflexivity.
omega.
Qed.
-
+
Let ZNWord sz x := Word.NToWord sz (BinInt.Z.to_N x).
Lemma combine_ZNWord : forall sz1 sz2 z1 z2,
(0 <= Z.of_nat sz1)%Z ->