From 75cf217c2a60422e2ae7ee56d177b140f8b47924 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 30 Oct 2016 21:31:11 -0400 Subject: Remove an [About] --- src/Reflection/Z/Interpretations.v | 1 - 1 file changed, 1 deletion(-) (limited to 'src/Reflection') diff --git a/src/Reflection/Z/Interpretations.v b/src/Reflection/Z/Interpretations.v index 0033e3360..0c9a18c79 100644 --- a/src/Reflection/Z/Interpretations.v +++ b/src/Reflection/Z/Interpretations.v @@ -279,7 +279,6 @@ Module BoundedWord64. | TZ => t end. -About Sumbool.sumbool_of_bool. Definition word64ToBoundedWord (x : Word64.word64) : t. Proof. refine (let v := Word64.word64ToZ x in -- cgit v1.2.3