aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
diff options
context:
space:
mode:
authorPierre Roux2020-10-28 10:32:58 +0100
committerPierre Roux2020-11-05 00:20:53 +0100
commit36ac26532028bfc6f84e4dfc849b51f42a3d8286 (patch)
tree9a8057cf3171c7b8fcf1ca2aa452cddb3d14e0fc /doc/sphinx
parente3593abd322acb59c512b5f2f776091546b38887 (diff)
Rename Dec and HexDec to Decimal and Hexadecimal
As noted by Hugo Herbelin, Dec is rather used for "decidable".
Diffstat (limited to 'doc/sphinx')
-rw-r--r--doc/sphinx/user-extensions/syntax-extensions.rst4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 2af40792df..9d1fcc160d 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1884,7 +1884,7 @@ The following errors apply to both string and number notations:
| _ => None end in
f (Decimal.rev u).
Definition of_uint (u : Number.uint) : option radix3 :=
- match u with Number.UIntDec u => of_uint_dec u | Number.UIntHex _ => None end.
+ match u with Number.UIntDecimal u => of_uint_dec u | Number.UIntHexadecimal _ => None end.
and a printing function
@@ -1897,7 +1897,7 @@ The following errors apply to both string and number notations:
| x3p1 x => Decimal.D1 (f x)
| x3p2 x => Decimal.D2 (f x) end in
Decimal.rev (f x).
- Definition to_uint (x : radix3) : Number.uint := Number.UIntDec (to_uint_dec x).
+ Definition to_uint (x : radix3) : Number.uint := Number.UIntDecimal (to_uint_dec x).
before declaring the notation