From 36ac26532028bfc6f84e4dfc849b51f42a3d8286 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 28 Oct 2020 10:32:58 +0100 Subject: Rename Dec and HexDec to Decimal and Hexadecimal As noted by Hugo Herbelin, Dec is rather used for "decidable". --- doc/sphinx/user-extensions/syntax-extensions.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc/sphinx/user-extensions') 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 -- cgit v1.2.3