diff options
| author | Pierre Roux | 2020-10-28 10:32:58 +0100 |
|---|---|---|
| committer | Pierre Roux | 2020-11-05 00:20:53 +0100 |
| commit | 36ac26532028bfc6f84e4dfc849b51f42a3d8286 (patch) | |
| tree | 9a8057cf3171c7b8fcf1ca2aa452cddb3d14e0fc /theories/NArith | |
| parent | e3593abd322acb59c512b5f2f776091546b38887 (diff) | |
Rename Dec and HexDec to Decimal and Hexadecimal
As noted by Hugo Herbelin, Dec is rather used for "decidable".
Diffstat (limited to 'theories/NArith')
| -rw-r--r-- | theories/NArith/BinNatDef.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index 4142bb786f..e57e5fe856 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -392,8 +392,8 @@ Definition of_hex_uint (d:Hexadecimal.uint) := Pos.of_hex_uint d. Definition of_num_uint (d:Number.uint) := match d with - | Number.UIntDec d => of_uint d - | Number.UIntHex d => of_hex_uint d + | Number.UIntDecimal d => of_uint d + | Number.UIntHexadecimal d => of_hex_uint d end. Definition of_int (d:Decimal.int) := @@ -410,8 +410,8 @@ Definition of_hex_int (d:Hexadecimal.int) := Definition of_num_int (d:Number.int) := match d with - | Number.IntDec d => of_int d - | Number.IntHex d => of_hex_int d + | Number.IntDecimal d => of_int d + | Number.IntHexadecimal d => of_hex_int d end. Definition to_uint n := @@ -426,13 +426,13 @@ Definition to_hex_uint n := | pos p => Pos.to_hex_uint p end. -Definition to_num_uint n := Number.UIntDec (to_uint n). +Definition to_num_uint n := Number.UIntDecimal (to_uint n). Definition to_int n := Decimal.Pos (to_uint n). Definition to_hex_int n := Hexadecimal.Pos (to_hex_uint n). -Definition to_num_int n := Number.IntDec (to_int n). +Definition to_num_int n := Number.IntDecimal (to_int n). Number Notation N of_num_uint to_num_uint : N_scope. |