diff options
| author | Pierre Roux | 2020-09-03 13:26:00 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-11-05 00:20:19 +0100 |
| commit | 3b766fd8859b692e3e93cf83bf87d393e32c572e (patch) | |
| tree | c241d8dcd7a8e725f06013558dfb66946dec5e87 /theories/Init | |
| parent | e728a1ef0f8b5fdc4b1815a7d0349c67db15f9b4 (diff) | |
Merge numeral and string notation plugins
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Byte.v | 2 | ||||
| -rw-r--r-- | theories/Init/Prelude.v | 2 |
2 files changed, 1 insertions, 3 deletions
diff --git a/theories/Init/Byte.v b/theories/Init/Byte.v index 7449b52d76..e03820ef22 100644 --- a/theories/Init/Byte.v +++ b/theories/Init/Byte.v @@ -16,7 +16,7 @@ Require Import Coq.Init.Logic. Require Import Coq.Init.Specif. Require Coq.Init.Nat. -Declare ML Module "string_notation_plugin". +Declare ML Module "number_string_notation_plugin". (** We define an inductive for use with the [String Notation] command which contains all ascii characters. We use 256 constructors for diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 0239778bac..9f8a054b5c 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -30,8 +30,6 @@ Require Export Coq.Init.Tauto. *) Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". -Declare ML Module "numeral_notation_plugin". -Declare ML Module "string_notation_plugin". (* Parsing / printing of hexadecimal numbers *) Arguments Nat.of_hex_uint d%hex_uint_scope. |