diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-30 21:31:11 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-30 21:31:11 -0400 |
| commit | 75cf217c2a60422e2ae7ee56d177b140f8b47924 (patch) | |
| tree | 88af06a93952def6e20f040f6c18ece81512876f /src | |
| parent | bef02d299d3b501776bc5e7c67cb82e44cdce8b6 (diff) | |
Remove an [About]
Diffstat (limited to 'src')
| -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 |