diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Init/Decimal.v | 6 | ||||
| -rw-r--r-- | theories/Init/Prelude.v | 10 |
2 files changed, 16 insertions, 0 deletions
diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index 57163b1b07..34b4e75814 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.v @@ -161,3 +161,9 @@ with succ_double d := end. End Little. + +(** Pseudo-conversion functions used when declaring + Numeral Notations on [uint] and [int]. *) + +Definition uint_of_uint (i:uint) := i. +Definition int_of_int (i:int) := i. diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 390ff5e240..f99a6a7c60 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -26,5 +26,15 @@ Require Export Coq.Init.Tauto. *) Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". +Declare ML Module "numeral_notation_plugin". + +(* Parsing / printing of decimal numbers *) +Arguments Nat.of_uint d%uint_scope. +Arguments Nat.of_int d%int_scope. +Numeral Notation Decimal.uint Decimal.uint_of_uint Decimal.uint_of_uint + : uint_scope. +Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int + : int_scope. + (* Default substrings not considered by queries like SearchAbout *) Add Search Blacklist "_subproof" "_subterm" "Private_". |