diff options
Diffstat (limited to 'src/Reflection/Z/Interpretations.v')
| -rw-r--r-- | src/Reflection/Z/Interpretations.v | 1 |
1 files changed, 0 insertions, 1 deletions
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 |