Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`

5 files changed, 2179 insertions, 24 deletions

diff --git a/theories/Init/Byte.v b/theories/Init/Byte.v
new file mode 100644
index 0000000000..eede9d5028
--- /dev/null
+++ b/theories/Init/Byte.v
@@ -0,0 +1,830 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** * Bytes *)
+
+Require Import Coq.Init.Datatypes.
+Require Import Coq.Init.Logic.
+Require Import Coq.Init.Specif.
+Require Coq.Init.Nat.
+
+Declare ML Module "string_notation_plugin".
+
+(** We define an inductive for use with the [String Notation] command
+    which contains all ascii characters.  We use 256 constructors for
+    efficiency and ease of conversion. *)
+
+Declare Scope byte_scope.
+Delimit Scope byte_scope with byte.
+
+Inductive byte :=
+| x00
+| x01
+| x02
+| x03
+| x04
+| x05
+| x06
+| x07
+| x08
+| x09
+| x0a
+| x0b
+| x0c
+| x0d
+| x0e
+| x0f
+| x10
+| x11
+| x12
+| x13
+| x14
+| x15
+| x16
+| x17
+| x18
+| x19
+| x1a
+| x1b
+| x1c
+| x1d
+| x1e
+| x1f
+| x20
+| x21
+| x22
+| x23
+| x24
+| x25
+| x26
+| x27
+| x28
+| x29
+| x2a
+| x2b
+| x2c
+| x2d
+| x2e
+| x2f
+| x30
+| x31
+| x32
+| x33
+| x34
+| x35
+| x36
+| x37
+| x38
+| x39
+| x3a
+| x3b
+| x3c
+| x3d
+| x3e
+| x3f
+| x40
+| x41
+| x42
+| x43
+| x44
+| x45
+| x46
+| x47
+| x48
+| x49
+| x4a
+| x4b
+| x4c
+| x4d
+| x4e
+| x4f
+| x50
+| x51
+| x52
+| x53
+| x54
+| x55
+| x56
+| x57
+| x58
+| x59
+| x5a
+| x5b
+| x5c
+| x5d
+| x5e
+| x5f
+| x60
+| x61
+| x62
+| x63
+| x64
+| x65
+| x66
+| x67
+| x68
+| x69
+| x6a
+| x6b
+| x6c
+| x6d
+| x6e
+| x6f
+| x70
+| x71
+| x72
+| x73
+| x74
+| x75
+| x76
+| x77
+| x78
+| x79
+| x7a
+| x7b
+| x7c
+| x7d
+| x7e
+| x7f
+| x80
+| x81
+| x82
+| x83
+| x84
+| x85
+| x86
+| x87
+| x88
+| x89
+| x8a
+| x8b
+| x8c
+| x8d
+| x8e
+| x8f
+| x90
+| x91
+| x92
+| x93
+| x94
+| x95
+| x96
+| x97
+| x98
+| x99
+| x9a
+| x9b
+| x9c
+| x9d
+| x9e
+| x9f
+| xa0
+| xa1
+| xa2
+| xa3
+| xa4
+| xa5
+| xa6
+| xa7
+| xa8
+| xa9
+| xaa
+| xab
+| xac
+| xad
+| xae
+| xaf
+| xb0
+| xb1
+| xb2
+| xb3
+| xb4
+| xb5
+| xb6
+| xb7
+| xb8
+| xb9
+| xba
+| xbb
+| xbc
+| xbd
+| xbe
+| xbf
+| xc0
+| xc1
+| xc2
+| xc3
+| xc4
+| xc5
+| xc6
+| xc7
+| xc8
+| xc9
+| xca
+| xcb
+| xcc
+| xcd
+| xce
+| xcf
+| xd0
+| xd1
+| xd2
+| xd3
+| xd4
+| xd5
+| xd6
+| xd7
+| xd8
+| xd9
+| xda
+| xdb
+| xdc
+| xdd
+| xde
+| xdf
+| xe0
+| xe1
+| xe2
+| xe3
+| xe4
+| xe5
+| xe6
+| xe7
+| xe8
+| xe9
+| xea
+| xeb
+| xec
+| xed
+| xee
+| xef
+| xf0
+| xf1
+| xf2
+| xf3
+| xf4
+| xf5
+| xf6
+| xf7
+| xf8
+| xf9
+| xfa
+| xfb
+| xfc
+| xfd
+| xfe
+| xff
+.
+
+Bind Scope byte_scope with byte.
+
+Register byte as core.byte.type.
+
+Local Notation "0" := false.
+Local Notation "1" := true.
+
+(** We pick a definition that matches with [Ascii.ascii] *)
+Definition of_bits (b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))) : byte
+  := match b with
+     | (0,(0,(0,(0,(0,(0,(0,0))))))) => x00
+     | (1,(0,(0,(0,(0,(0,(0,0))))))) => x01
+     | (0,(1,(0,(0,(0,(0,(0,0))))))) => x02
+     | (1,(1,(0,(0,(0,(0,(0,0))))))) => x03
+     | (0,(0,(1,(0,(0,(0,(0,0))))))) => x04
+     | (1,(0,(1,(0,(0,(0,(0,0))))))) => x05
+     | (0,(1,(1,(0,(0,(0,(0,0))))))) => x06
+     | (1,(1,(1,(0,(0,(0,(0,0))))))) => x07
+     | (0,(0,(0,(1,(0,(0,(0,0))))))) => x08
+     | (1,(0,(0,(1,(0,(0,(0,0))))))) => x09
+     | (0,(1,(0,(1,(0,(0,(0,0))))))) => x0a
+     | (1,(1,(0,(1,(0,(0,(0,0))))))) => x0b
+     | (0,(0,(1,(1,(0,(0,(0,0))))))) => x0c
+     | (1,(0,(1,(1,(0,(0,(0,0))))))) => x0d
+     | (0,(1,(1,(1,(0,(0,(0,0))))))) => x0e
+     | (1,(1,(1,(1,(0,(0,(0,0))))))) => x0f
+     | (0,(0,(0,(0,(1,(0,(0,0))))))) => x10
+     | (1,(0,(0,(0,(1,(0,(0,0))))))) => x11
+     | (0,(1,(0,(0,(1,(0,(0,0))))))) => x12
+     | (1,(1,(0,(0,(1,(0,(0,0))))))) => x13
+     | (0,(0,(1,(0,(1,(0,(0,0))))))) => x14
+     | (1,(0,(1,(0,(1,(0,(0,0))))))) => x15
+     | (0,(1,(1,(0,(1,(0,(0,0))))))) => x16
+     | (1,(1,(1,(0,(1,(0,(0,0))))))) => x17
+     | (0,(0,(0,(1,(1,(0,(0,0))))))) => x18
+     | (1,(0,(0,(1,(1,(0,(0,0))))))) => x19
+     | (0,(1,(0,(1,(1,(0,(0,0))))))) => x1a
+     | (1,(1,(0,(1,(1,(0,(0,0))))))) => x1b
+     | (0,(0,(1,(1,(1,(0,(0,0))))))) => x1c
+     | (1,(0,(1,(1,(1,(0,(0,0))))))) => x1d
+     | (0,(1,(1,(1,(1,(0,(0,0))))))) => x1e
+     | (1,(1,(1,(1,(1,(0,(0,0))))))) => x1f
+     | (0,(0,(0,(0,(0,(1,(0,0))))))) => x20
+     | (1,(0,(0,(0,(0,(1,(0,0))))))) => x21
+     | (0,(1,(0,(0,(0,(1,(0,0))))))) => x22
+     | (1,(1,(0,(0,(0,(1,(0,0))))))) => x23
+     | (0,(0,(1,(0,(0,(1,(0,0))))))) => x24
+     | (1,(0,(1,(0,(0,(1,(0,0))))))) => x25
+     | (0,(1,(1,(0,(0,(1,(0,0))))))) => x26
+     | (1,(1,(1,(0,(0,(1,(0,0))))))) => x27
+     | (0,(0,(0,(1,(0,(1,(0,0))))))) => x28
+     | (1,(0,(0,(1,(0,(1,(0,0))))))) => x29
+     | (0,(1,(0,(1,(0,(1,(0,0))))))) => x2a
+     | (1,(1,(0,(1,(0,(1,(0,0))))))) => x2b
+     | (0,(0,(1,(1,(0,(1,(0,0))))))) => x2c
+     | (1,(0,(1,(1,(0,(1,(0,0))))))) => x2d
+     | (0,(1,(1,(1,(0,(1,(0,0))))))) => x2e
+     | (1,(1,(1,(1,(0,(1,(0,0))))))) => x2f
+     | (0,(0,(0,(0,(1,(1,(0,0))))))) => x30
+     | (1,(0,(0,(0,(1,(1,(0,0))))))) => x31
+     | (0,(1,(0,(0,(1,(1,(0,0))))))) => x32
+     | (1,(1,(0,(0,(1,(1,(0,0))))))) => x33
+     | (0,(0,(1,(0,(1,(1,(0,0))))))) => x34
+     | (1,(0,(1,(0,(1,(1,(0,0))))))) => x35
+     | (0,(1,(1,(0,(1,(1,(0,0))))))) => x36
+     | (1,(1,(1,(0,(1,(1,(0,0))))))) => x37
+     | (0,(0,(0,(1,(1,(1,(0,0))))))) => x38
+     | (1,(0,(0,(1,(1,(1,(0,0))))))) => x39
+     | (0,(1,(0,(1,(1,(1,(0,0))))))) => x3a
+     | (1,(1,(0,(1,(1,(1,(0,0))))))) => x3b
+     | (0,(0,(1,(1,(1,(1,(0,0))))))) => x3c
+     | (1,(0,(1,(1,(1,(1,(0,0))))))) => x3d
+     | (0,(1,(1,(1,(1,(1,(0,0))))))) => x3e
+     | (1,(1,(1,(1,(1,(1,(0,0))))))) => x3f
+     | (0,(0,(0,(0,(0,(0,(1,0))))))) => x40
+     | (1,(0,(0,(0,(0,(0,(1,0))))))) => x41
+     | (0,(1,(0,(0,(0,(0,(1,0))))))) => x42
+     | (1,(1,(0,(0,(0,(0,(1,0))))))) => x43
+     | (0,(0,(1,(0,(0,(0,(1,0))))))) => x44
+     | (1,(0,(1,(0,(0,(0,(1,0))))))) => x45
+     | (0,(1,(1,(0,(0,(0,(1,0))))))) => x46
+     | (1,(1,(1,(0,(0,(0,(1,0))))))) => x47
+     | (0,(0,(0,(1,(0,(0,(1,0))))))) => x48
+     | (1,(0,(0,(1,(0,(0,(1,0))))))) => x49
+     | (0,(1,(0,(1,(0,(0,(1,0))))))) => x4a
+     | (1,(1,(0,(1,(0,(0,(1,0))))))) => x4b
+     | (0,(0,(1,(1,(0,(0,(1,0))))))) => x4c
+     | (1,(0,(1,(1,(0,(0,(1,0))))))) => x4d
+     | (0,(1,(1,(1,(0,(0,(1,0))))))) => x4e
+     | (1,(1,(1,(1,(0,(0,(1,0))))))) => x4f
+     | (0,(0,(0,(0,(1,(0,(1,0))))))) => x50
+     | (1,(0,(0,(0,(1,(0,(1,0))))))) => x51
+     | (0,(1,(0,(0,(1,(0,(1,0))))))) => x52
+     | (1,(1,(0,(0,(1,(0,(1,0))))))) => x53
+     | (0,(0,(1,(0,(1,(0,(1,0))))))) => x54
+     | (1,(0,(1,(0,(1,(0,(1,0))))))) => x55
+     | (0,(1,(1,(0,(1,(0,(1,0))))))) => x56
+     | (1,(1,(1,(0,(1,(0,(1,0))))))) => x57
+     | (0,(0,(0,(1,(1,(0,(1,0))))))) => x58
+     | (1,(0,(0,(1,(1,(0,(1,0))))))) => x59
+     | (0,(1,(0,(1,(1,(0,(1,0))))))) => x5a
+     | (1,(1,(0,(1,(1,(0,(1,0))))))) => x5b
+     | (0,(0,(1,(1,(1,(0,(1,0))))))) => x5c
+     | (1,(0,(1,(1,(1,(0,(1,0))))))) => x5d
+     | (0,(1,(1,(1,(1,(0,(1,0))))))) => x5e
+     | (1,(1,(1,(1,(1,(0,(1,0))))))) => x5f
+     | (0,(0,(0,(0,(0,(1,(1,0))))))) => x60
+     | (1,(0,(0,(0,(0,(1,(1,0))))))) => x61
+     | (0,(1,(0,(0,(0,(1,(1,0))))))) => x62
+     | (1,(1,(0,(0,(0,(1,(1,0))))))) => x63
+     | (0,(0,(1,(0,(0,(1,(1,0))))))) => x64
+     | (1,(0,(1,(0,(0,(1,(1,0))))))) => x65
+     | (0,(1,(1,(0,(0,(1,(1,0))))))) => x66
+     | (1,(1,(1,(0,(0,(1,(1,0))))))) => x67
+     | (0,(0,(0,(1,(0,(1,(1,0))))))) => x68
+     | (1,(0,(0,(1,(0,(1,(1,0))))))) => x69
+     | (0,(1,(0,(1,(0,(1,(1,0))))))) => x6a
+     | (1,(1,(0,(1,(0,(1,(1,0))))))) => x6b
+     | (0,(0,(1,(1,(0,(1,(1,0))))))) => x6c
+     | (1,(0,(1,(1,(0,(1,(1,0))))))) => x6d
+     | (0,(1,(1,(1,(0,(1,(1,0))))))) => x6e
+     | (1,(1,(1,(1,(0,(1,(1,0))))))) => x6f
+     | (0,(0,(0,(0,(1,(1,(1,0))))))) => x70
+     | (1,(0,(0,(0,(1,(1,(1,0))))))) => x71
+     | (0,(1,(0,(0,(1,(1,(1,0))))))) => x72
+     | (1,(1,(0,(0,(1,(1,(1,0))))))) => x73
+     | (0,(0,(1,(0,(1,(1,(1,0))))))) => x74
+     | (1,(0,(1,(0,(1,(1,(1,0))))))) => x75
+     | (0,(1,(1,(0,(1,(1,(1,0))))))) => x76
+     | (1,(1,(1,(0,(1,(1,(1,0))))))) => x77
+     | (0,(0,(0,(1,(1,(1,(1,0))))))) => x78
+     | (1,(0,(0,(1,(1,(1,(1,0))))))) => x79
+     | (0,(1,(0,(1,(1,(1,(1,0))))))) => x7a
+     | (1,(1,(0,(1,(1,(1,(1,0))))))) => x7b
+     | (0,(0,(1,(1,(1,(1,(1,0))))))) => x7c
+     | (1,(0,(1,(1,(1,(1,(1,0))))))) => x7d
+     | (0,(1,(1,(1,(1,(1,(1,0))))))) => x7e
+     | (1,(1,(1,(1,(1,(1,(1,0))))))) => x7f
+     | (0,(0,(0,(0,(0,(0,(0,1))))))) => x80
+     | (1,(0,(0,(0,(0,(0,(0,1))))))) => x81
+     | (0,(1,(0,(0,(0,(0,(0,1))))))) => x82
+     | (1,(1,(0,(0,(0,(0,(0,1))))))) => x83
+     | (0,(0,(1,(0,(0,(0,(0,1))))))) => x84
+     | (1,(0,(1,(0,(0,(0,(0,1))))))) => x85
+     | (0,(1,(1,(0,(0,(0,(0,1))))))) => x86
+     | (1,(1,(1,(0,(0,(0,(0,1))))))) => x87
+     | (0,(0,(0,(1,(0,(0,(0,1))))))) => x88
+     | (1,(0,(0,(1,(0,(0,(0,1))))))) => x89
+     | (0,(1,(0,(1,(0,(0,(0,1))))))) => x8a
+     | (1,(1,(0,(1,(0,(0,(0,1))))))) => x8b
+     | (0,(0,(1,(1,(0,(0,(0,1))))))) => x8c
+     | (1,(0,(1,(1,(0,(0,(0,1))))))) => x8d
+     | (0,(1,(1,(1,(0,(0,(0,1))))))) => x8e
+     | (1,(1,(1,(1,(0,(0,(0,1))))))) => x8f
+     | (0,(0,(0,(0,(1,(0,(0,1))))))) => x90
+     | (1,(0,(0,(0,(1,(0,(0,1))))))) => x91
+     | (0,(1,(0,(0,(1,(0,(0,1))))))) => x92
+     | (1,(1,(0,(0,(1,(0,(0,1))))))) => x93
+     | (0,(0,(1,(0,(1,(0,(0,1))))))) => x94
+     | (1,(0,(1,(0,(1,(0,(0,1))))))) => x95
+     | (0,(1,(1,(0,(1,(0,(0,1))))))) => x96
+     | (1,(1,(1,(0,(1,(0,(0,1))))))) => x97
+     | (0,(0,(0,(1,(1,(0,(0,1))))))) => x98
+     | (1,(0,(0,(1,(1,(0,(0,1))))))) => x99
+     | (0,(1,(0,(1,(1,(0,(0,1))))))) => x9a
+     | (1,(1,(0,(1,(1,(0,(0,1))))))) => x9b
+     | (0,(0,(1,(1,(1,(0,(0,1))))))) => x9c
+     | (1,(0,(1,(1,(1,(0,(0,1))))))) => x9d
+     | (0,(1,(1,(1,(1,(0,(0,1))))))) => x9e
+     | (1,(1,(1,(1,(1,(0,(0,1))))))) => x9f
+     | (0,(0,(0,(0,(0,(1,(0,1))))))) => xa0
+     | (1,(0,(0,(0,(0,(1,(0,1))))))) => xa1
+     | (0,(1,(0,(0,(0,(1,(0,1))))))) => xa2
+     | (1,(1,(0,(0,(0,(1,(0,1))))))) => xa3
+     | (0,(0,(1,(0,(0,(1,(0,1))))))) => xa4
+     | (1,(0,(1,(0,(0,(1,(0,1))))))) => xa5
+     | (0,(1,(1,(0,(0,(1,(0,1))))))) => xa6
+     | (1,(1,(1,(0,(0,(1,(0,1))))))) => xa7
+     | (0,(0,(0,(1,(0,(1,(0,1))))))) => xa8
+     | (1,(0,(0,(1,(0,(1,(0,1))))))) => xa9
+     | (0,(1,(0,(1,(0,(1,(0,1))))))) => xaa
+     | (1,(1,(0,(1,(0,(1,(0,1))))))) => xab
+     | (0,(0,(1,(1,(0,(1,(0,1))))))) => xac
+     | (1,(0,(1,(1,(0,(1,(0,1))))))) => xad
+     | (0,(1,(1,(1,(0,(1,(0,1))))))) => xae
+     | (1,(1,(1,(1,(0,(1,(0,1))))))) => xaf
+     | (0,(0,(0,(0,(1,(1,(0,1))))))) => xb0
+     | (1,(0,(0,(0,(1,(1,(0,1))))))) => xb1
+     | (0,(1,(0,(0,(1,(1,(0,1))))))) => xb2
+     | (1,(1,(0,(0,(1,(1,(0,1))))))) => xb3
+     | (0,(0,(1,(0,(1,(1,(0,1))))))) => xb4
+     | (1,(0,(1,(0,(1,(1,(0,1))))))) => xb5
+     | (0,(1,(1,(0,(1,(1,(0,1))))))) => xb6
+     | (1,(1,(1,(0,(1,(1,(0,1))))))) => xb7
+     | (0,(0,(0,(1,(1,(1,(0,1))))))) => xb8
+     | (1,(0,(0,(1,(1,(1,(0,1))))))) => xb9
+     | (0,(1,(0,(1,(1,(1,(0,1))))))) => xba
+     | (1,(1,(0,(1,(1,(1,(0,1))))))) => xbb
+     | (0,(0,(1,(1,(1,(1,(0,1))))))) => xbc
+     | (1,(0,(1,(1,(1,(1,(0,1))))))) => xbd
+     | (0,(1,(1,(1,(1,(1,(0,1))))))) => xbe
+     | (1,(1,(1,(1,(1,(1,(0,1))))))) => xbf
+     | (0,(0,(0,(0,(0,(0,(1,1))))))) => xc0
+     | (1,(0,(0,(0,(0,(0,(1,1))))))) => xc1
+     | (0,(1,(0,(0,(0,(0,(1,1))))))) => xc2
+     | (1,(1,(0,(0,(0,(0,(1,1))))))) => xc3
+     | (0,(0,(1,(0,(0,(0,(1,1))))))) => xc4
+     | (1,(0,(1,(0,(0,(0,(1,1))))))) => xc5
+     | (0,(1,(1,(0,(0,(0,(1,1))))))) => xc6
+     | (1,(1,(1,(0,(0,(0,(1,1))))))) => xc7
+     | (0,(0,(0,(1,(0,(0,(1,1))))))) => xc8
+     | (1,(0,(0,(1,(0,(0,(1,1))))))) => xc9
+     | (0,(1,(0,(1,(0,(0,(1,1))))))) => xca
+     | (1,(1,(0,(1,(0,(0,(1,1))))))) => xcb
+     | (0,(0,(1,(1,(0,(0,(1,1))))))) => xcc
+     | (1,(0,(1,(1,(0,(0,(1,1))))))) => xcd
+     | (0,(1,(1,(1,(0,(0,(1,1))))))) => xce
+     | (1,(1,(1,(1,(0,(0,(1,1))))))) => xcf
+     | (0,(0,(0,(0,(1,(0,(1,1))))))) => xd0
+     | (1,(0,(0,(0,(1,(0,(1,1))))))) => xd1
+     | (0,(1,(0,(0,(1,(0,(1,1))))))) => xd2
+     | (1,(1,(0,(0,(1,(0,(1,1))))))) => xd3
+     | (0,(0,(1,(0,(1,(0,(1,1))))))) => xd4
+     | (1,(0,(1,(0,(1,(0,(1,1))))))) => xd5
+     | (0,(1,(1,(0,(1,(0,(1,1))))))) => xd6
+     | (1,(1,(1,(0,(1,(0,(1,1))))))) => xd7
+     | (0,(0,(0,(1,(1,(0,(1,1))))))) => xd8
+     | (1,(0,(0,(1,(1,(0,(1,1))))))) => xd9
+     | (0,(1,(0,(1,(1,(0,(1,1))))))) => xda
+     | (1,(1,(0,(1,(1,(0,(1,1))))))) => xdb
+     | (0,(0,(1,(1,(1,(0,(1,1))))))) => xdc
+     | (1,(0,(1,(1,(1,(0,(1,1))))))) => xdd
+     | (0,(1,(1,(1,(1,(0,(1,1))))))) => xde
+     | (1,(1,(1,(1,(1,(0,(1,1))))))) => xdf
+     | (0,(0,(0,(0,(0,(1,(1,1))))))) => xe0
+     | (1,(0,(0,(0,(0,(1,(1,1))))))) => xe1
+     | (0,(1,(0,(0,(0,(1,(1,1))))))) => xe2
+     | (1,(1,(0,(0,(0,(1,(1,1))))))) => xe3
+     | (0,(0,(1,(0,(0,(1,(1,1))))))) => xe4
+     | (1,(0,(1,(0,(0,(1,(1,1))))))) => xe5
+     | (0,(1,(1,(0,(0,(1,(1,1))))))) => xe6
+     | (1,(1,(1,(0,(0,(1,(1,1))))))) => xe7
+     | (0,(0,(0,(1,(0,(1,(1,1))))))) => xe8
+     | (1,(0,(0,(1,(0,(1,(1,1))))))) => xe9
+     | (0,(1,(0,(1,(0,(1,(1,1))))))) => xea
+     | (1,(1,(0,(1,(0,(1,(1,1))))))) => xeb
+     | (0,(0,(1,(1,(0,(1,(1,1))))))) => xec
+     | (1,(0,(1,(1,(0,(1,(1,1))))))) => xed
+     | (0,(1,(1,(1,(0,(1,(1,1))))))) => xee
+     | (1,(1,(1,(1,(0,(1,(1,1))))))) => xef
+     | (0,(0,(0,(0,(1,(1,(1,1))))))) => xf0
+     | (1,(0,(0,(0,(1,(1,(1,1))))))) => xf1
+     | (0,(1,(0,(0,(1,(1,(1,1))))))) => xf2
+     | (1,(1,(0,(0,(1,(1,(1,1))))))) => xf3
+     | (0,(0,(1,(0,(1,(1,(1,1))))))) => xf4
+     | (1,(0,(1,(0,(1,(1,(1,1))))))) => xf5
+     | (0,(1,(1,(0,(1,(1,(1,1))))))) => xf6
+     | (1,(1,(1,(0,(1,(1,(1,1))))))) => xf7
+     | (0,(0,(0,(1,(1,(1,(1,1))))))) => xf8
+     | (1,(0,(0,(1,(1,(1,(1,1))))))) => xf9
+     | (0,(1,(0,(1,(1,(1,(1,1))))))) => xfa
+     | (1,(1,(0,(1,(1,(1,(1,1))))))) => xfb
+     | (0,(0,(1,(1,(1,(1,(1,1))))))) => xfc
+     | (1,(0,(1,(1,(1,(1,(1,1))))))) => xfd
+     | (0,(1,(1,(1,(1,(1,(1,1))))))) => xfe
+     | (1,(1,(1,(1,(1,(1,(1,1))))))) => xff
+     end.
+
+Definition to_bits (b : byte) : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
+  := match b with
+     | x00 => (0,(0,(0,(0,(0,(0,(0,0)))))))
+     | x01 => (1,(0,(0,(0,(0,(0,(0,0)))))))
+     | x02 => (0,(1,(0,(0,(0,(0,(0,0)))))))
+     | x03 => (1,(1,(0,(0,(0,(0,(0,0)))))))
+     | x04 => (0,(0,(1,(0,(0,(0,(0,0)))))))
+     | x05 => (1,(0,(1,(0,(0,(0,(0,0)))))))
+     | x06 => (0,(1,(1,(0,(0,(0,(0,0)))))))
+     | x07 => (1,(1,(1,(0,(0,(0,(0,0)))))))
+     | x08 => (0,(0,(0,(1,(0,(0,(0,0)))))))
+     | x09 => (1,(0,(0,(1,(0,(0,(0,0)))))))
+     | x0a => (0,(1,(0,(1,(0,(0,(0,0)))))))
+     | x0b => (1,(1,(0,(1,(0,(0,(0,0)))))))
+     | x0c => (0,(0,(1,(1,(0,(0,(0,0)))))))
+     | x0d => (1,(0,(1,(1,(0,(0,(0,0)))))))
+     | x0e => (0,(1,(1,(1,(0,(0,(0,0)))))))
+     | x0f => (1,(1,(1,(1,(0,(0,(0,0)))))))
+     | x10 => (0,(0,(0,(0,(1,(0,(0,0)))))))
+     | x11 => (1,(0,(0,(0,(1,(0,(0,0)))))))
+     | x12 => (0,(1,(0,(0,(1,(0,(0,0)))))))
+     | x13 => (1,(1,(0,(0,(1,(0,(0,0)))))))
+     | x14 => (0,(0,(1,(0,(1,(0,(0,0)))))))
+     | x15 => (1,(0,(1,(0,(1,(0,(0,0)))))))
+     | x16 => (0,(1,(1,(0,(1,(0,(0,0)))))))
+     | x17 => (1,(1,(1,(0,(1,(0,(0,0)))))))
+     | x18 => (0,(0,(0,(1,(1,(0,(0,0)))))))
+     | x19 => (1,(0,(0,(1,(1,(0,(0,0)))))))
+     | x1a => (0,(1,(0,(1,(1,(0,(0,0)))))))
+     | x1b => (1,(1,(0,(1,(1,(0,(0,0)))))))
+     | x1c => (0,(0,(1,(1,(1,(0,(0,0)))))))
+     | x1d => (1,(0,(1,(1,(1,(0,(0,0)))))))
+     | x1e => (0,(1,(1,(1,(1,(0,(0,0)))))))
+     | x1f => (1,(1,(1,(1,(1,(0,(0,0)))))))
+     | x20 => (0,(0,(0,(0,(0,(1,(0,0)))))))
+     | x21 => (1,(0,(0,(0,(0,(1,(0,0)))))))
+     | x22 => (0,(1,(0,(0,(0,(1,(0,0)))))))
+     | x23 => (1,(1,(0,(0,(0,(1,(0,0)))))))
+     | x24 => (0,(0,(1,(0,(0,(1,(0,0)))))))
+     | x25 => (1,(0,(1,(0,(0,(1,(0,0)))))))
+     | x26 => (0,(1,(1,(0,(0,(1,(0,0)))))))
+     | x27 => (1,(1,(1,(0,(0,(1,(0,0)))))))
+     | x28 => (0,(0,(0,(1,(0,(1,(0,0)))))))
+     | x29 => (1,(0,(0,(1,(0,(1,(0,0)))))))
+     | x2a => (0,(1,(0,(1,(0,(1,(0,0)))))))
+     | x2b => (1,(1,(0,(1,(0,(1,(0,0)))))))
+     | x2c => (0,(0,(1,(1,(0,(1,(0,0)))))))
+     | x2d => (1,(0,(1,(1,(0,(1,(0,0)))))))
+     | x2e => (0,(1,(1,(1,(0,(1,(0,0)))))))
+     | x2f => (1,(1,(1,(1,(0,(1,(0,0)))))))
+     | x30 => (0,(0,(0,(0,(1,(1,(0,0)))))))
+     | x31 => (1,(0,(0,(0,(1,(1,(0,0)))))))
+     | x32 => (0,(1,(0,(0,(1,(1,(0,0)))))))
+     | x33 => (1,(1,(0,(0,(1,(1,(0,0)))))))
+     | x34 => (0,(0,(1,(0,(1,(1,(0,0)))))))
+     | x35 => (1,(0,(1,(0,(1,(1,(0,0)))))))
+     | x36 => (0,(1,(1,(0,(1,(1,(0,0)))))))
+     | x37 => (1,(1,(1,(0,(1,(1,(0,0)))))))
+     | x38 => (0,(0,(0,(1,(1,(1,(0,0)))))))
+     | x39 => (1,(0,(0,(1,(1,(1,(0,0)))))))
+     | x3a => (0,(1,(0,(1,(1,(1,(0,0)))))))
+     | x3b => (1,(1,(0,(1,(1,(1,(0,0)))))))
+     | x3c => (0,(0,(1,(1,(1,(1,(0,0)))))))
+     | x3d => (1,(0,(1,(1,(1,(1,(0,0)))))))
+     | x3e => (0,(1,(1,(1,(1,(1,(0,0)))))))
+     | x3f => (1,(1,(1,(1,(1,(1,(0,0)))))))
+     | x40 => (0,(0,(0,(0,(0,(0,(1,0)))))))
+     | x41 => (1,(0,(0,(0,(0,(0,(1,0)))))))
+     | x42 => (0,(1,(0,(0,(0,(0,(1,0)))))))
+     | x43 => (1,(1,(0,(0,(0,(0,(1,0)))))))
+     | x44 => (0,(0,(1,(0,(0,(0,(1,0)))))))
+     | x45 => (1,(0,(1,(0,(0,(0,(1,0)))))))
+     | x46 => (0,(1,(1,(0,(0,(0,(1,0)))))))
+     | x47 => (1,(1,(1,(0,(0,(0,(1,0)))))))
+     | x48 => (0,(0,(0,(1,(0,(0,(1,0)))))))
+     | x49 => (1,(0,(0,(1,(0,(0,(1,0)))))))
+     | x4a => (0,(1,(0,(1,(0,(0,(1,0)))))))
+     | x4b => (1,(1,(0,(1,(0,(0,(1,0)))))))
+     | x4c => (0,(0,(1,(1,(0,(0,(1,0)))))))
+     | x4d => (1,(0,(1,(1,(0,(0,(1,0)))))))
+     | x4e => (0,(1,(1,(1,(0,(0,(1,0)))))))
+     | x4f => (1,(1,(1,(1,(0,(0,(1,0)))))))
+     | x50 => (0,(0,(0,(0,(1,(0,(1,0)))))))
+     | x51 => (1,(0,(0,(0,(1,(0,(1,0)))))))
+     | x52 => (0,(1,(0,(0,(1,(0,(1,0)))))))
+     | x53 => (1,(1,(0,(0,(1,(0,(1,0)))))))
+     | x54 => (0,(0,(1,(0,(1,(0,(1,0)))))))
+     | x55 => (1,(0,(1,(0,(1,(0,(1,0)))))))
+     | x56 => (0,(1,(1,(0,(1,(0,(1,0)))))))
+     | x57 => (1,(1,(1,(0,(1,(0,(1,0)))))))
+     | x58 => (0,(0,(0,(1,(1,(0,(1,0)))))))
+     | x59 => (1,(0,(0,(1,(1,(0,(1,0)))))))
+     | x5a => (0,(1,(0,(1,(1,(0,(1,0)))))))
+     | x5b => (1,(1,(0,(1,(1,(0,(1,0)))))))
+     | x5c => (0,(0,(1,(1,(1,(0,(1,0)))))))
+     | x5d => (1,(0,(1,(1,(1,(0,(1,0)))))))
+     | x5e => (0,(1,(1,(1,(1,(0,(1,0)))))))
+     | x5f => (1,(1,(1,(1,(1,(0,(1,0)))))))
+     | x60 => (0,(0,(0,(0,(0,(1,(1,0)))))))
+     | x61 => (1,(0,(0,(0,(0,(1,(1,0)))))))
+     | x62 => (0,(1,(0,(0,(0,(1,(1,0)))))))
+     | x63 => (1,(1,(0,(0,(0,(1,(1,0)))))))
+     | x64 => (0,(0,(1,(0,(0,(1,(1,0)))))))
+     | x65 => (1,(0,(1,(0,(0,(1,(1,0)))))))
+     | x66 => (0,(1,(1,(0,(0,(1,(1,0)))))))
+     | x67 => (1,(1,(1,(0,(0,(1,(1,0)))))))
+     | x68 => (0,(0,(0,(1,(0,(1,(1,0)))))))
+     | x69 => (1,(0,(0,(1,(0,(1,(1,0)))))))
+     | x6a => (0,(1,(0,(1,(0,(1,(1,0)))))))
+     | x6b => (1,(1,(0,(1,(0,(1,(1,0)))))))
+     | x6c => (0,(0,(1,(1,(0,(1,(1,0)))))))
+     | x6d => (1,(0,(1,(1,(0,(1,(1,0)))))))
+     | x6e => (0,(1,(1,(1,(0,(1,(1,0)))))))
+     | x6f => (1,(1,(1,(1,(0,(1,(1,0)))))))
+     | x70 => (0,(0,(0,(0,(1,(1,(1,0)))))))
+     | x71 => (1,(0,(0,(0,(1,(1,(1,0)))))))
+     | x72 => (0,(1,(0,(0,(1,(1,(1,0)))))))
+     | x73 => (1,(1,(0,(0,(1,(1,(1,0)))))))
+     | x74 => (0,(0,(1,(0,(1,(1,(1,0)))))))
+     | x75 => (1,(0,(1,(0,(1,(1,(1,0)))))))
+     | x76 => (0,(1,(1,(0,(1,(1,(1,0)))))))
+     | x77 => (1,(1,(1,(0,(1,(1,(1,0)))))))
+     | x78 => (0,(0,(0,(1,(1,(1,(1,0)))))))
+     | x79 => (1,(0,(0,(1,(1,(1,(1,0)))))))
+     | x7a => (0,(1,(0,(1,(1,(1,(1,0)))))))
+     | x7b => (1,(1,(0,(1,(1,(1,(1,0)))))))
+     | x7c => (0,(0,(1,(1,(1,(1,(1,0)))))))
+     | x7d => (1,(0,(1,(1,(1,(1,(1,0)))))))
+     | x7e => (0,(1,(1,(1,(1,(1,(1,0)))))))
+     | x7f => (1,(1,(1,(1,(1,(1,(1,0)))))))
+     | x80 => (0,(0,(0,(0,(0,(0,(0,1)))))))
+     | x81 => (1,(0,(0,(0,(0,(0,(0,1)))))))
+     | x82 => (0,(1,(0,(0,(0,(0,(0,1)))))))
+     | x83 => (1,(1,(0,(0,(0,(0,(0,1)))))))
+     | x84 => (0,(0,(1,(0,(0,(0,(0,1)))))))
+     | x85 => (1,(0,(1,(0,(0,(0,(0,1)))))))
+     | x86 => (0,(1,(1,(0,(0,(0,(0,1)))))))
+     | x87 => (1,(1,(1,(0,(0,(0,(0,1)))))))
+     | x88 => (0,(0,(0,(1,(0,(0,(0,1)))))))
+     | x89 => (1,(0,(0,(1,(0,(0,(0,1)))))))
+     | x8a => (0,(1,(0,(1,(0,(0,(0,1)))))))
+     | x8b => (1,(1,(0,(1,(0,(0,(0,1)))))))
+     | x8c => (0,(0,(1,(1,(0,(0,(0,1)))))))
+     | x8d => (1,(0,(1,(1,(0,(0,(0,1)))))))
+     | x8e => (0,(1,(1,(1,(0,(0,(0,1)))))))
+     | x8f => (1,(1,(1,(1,(0,(0,(0,1)))))))
+     | x90 => (0,(0,(0,(0,(1,(0,(0,1)))))))
+     | x91 => (1,(0,(0,(0,(1,(0,(0,1)))))))
+     | x92 => (0,(1,(0,(0,(1,(0,(0,1)))))))
+     | x93 => (1,(1,(0,(0,(1,(0,(0,1)))))))
+     | x94 => (0,(0,(1,(0,(1,(0,(0,1)))))))
+     | x95 => (1,(0,(1,(0,(1,(0,(0,1)))))))
+     | x96 => (0,(1,(1,(0,(1,(0,(0,1)))))))
+     | x97 => (1,(1,(1,(0,(1,(0,(0,1)))))))
+     | x98 => (0,(0,(0,(1,(1,(0,(0,1)))))))
+     | x99 => (1,(0,(0,(1,(1,(0,(0,1)))))))
+     | x9a => (0,(1,(0,(1,(1,(0,(0,1)))))))
+     | x9b => (1,(1,(0,(1,(1,(0,(0,1)))))))
+     | x9c => (0,(0,(1,(1,(1,(0,(0,1)))))))
+     | x9d => (1,(0,(1,(1,(1,(0,(0,1)))))))
+     | x9e => (0,(1,(1,(1,(1,(0,(0,1)))))))
+     | x9f => (1,(1,(1,(1,(1,(0,(0,1)))))))
+     | xa0 => (0,(0,(0,(0,(0,(1,(0,1)))))))
+     | xa1 => (1,(0,(0,(0,(0,(1,(0,1)))))))
+     | xa2 => (0,(1,(0,(0,(0,(1,(0,1)))))))
+     | xa3 => (1,(1,(0,(0,(0,(1,(0,1)))))))
+     | xa4 => (0,(0,(1,(0,(0,(1,(0,1)))))))
+     | xa5 => (1,(0,(1,(0,(0,(1,(0,1)))))))
+     | xa6 => (0,(1,(1,(0,(0,(1,(0,1)))))))
+     | xa7 => (1,(1,(1,(0,(0,(1,(0,1)))))))
+     | xa8 => (0,(0,(0,(1,(0,(1,(0,1)))))))
+     | xa9 => (1,(0,(0,(1,(0,(1,(0,1)))))))
+     | xaa => (0,(1,(0,(1,(0,(1,(0,1)))))))
+     | xab => (1,(1,(0,(1,(0,(1,(0,1)))))))
+     | xac => (0,(0,(1,(1,(0,(1,(0,1)))))))
+     | xad => (1,(0,(1,(1,(0,(1,(0,1)))))))
+     | xae => (0,(1,(1,(1,(0,(1,(0,1)))))))
+     | xaf => (1,(1,(1,(1,(0,(1,(0,1)))))))
+     | xb0 => (0,(0,(0,(0,(1,(1,(0,1)))))))
+     | xb1 => (1,(0,(0,(0,(1,(1,(0,1)))))))
+     | xb2 => (0,(1,(0,(0,(1,(1,(0,1)))))))
+     | xb3 => (1,(1,(0,(0,(1,(1,(0,1)))))))
+     | xb4 => (0,(0,(1,(0,(1,(1,(0,1)))))))
+     | xb5 => (1,(0,(1,(0,(1,(1,(0,1)))))))
+     | xb6 => (0,(1,(1,(0,(1,(1,(0,1)))))))
+     | xb7 => (1,(1,(1,(0,(1,(1,(0,1)))))))
+     | xb8 => (0,(0,(0,(1,(1,(1,(0,1)))))))
+     | xb9 => (1,(0,(0,(1,(1,(1,(0,1)))))))
+     | xba => (0,(1,(0,(1,(1,(1,(0,1)))))))
+     | xbb => (1,(1,(0,(1,(1,(1,(0,1)))))))
+     | xbc => (0,(0,(1,(1,(1,(1,(0,1)))))))
+     | xbd => (1,(0,(1,(1,(1,(1,(0,1)))))))
+     | xbe => (0,(1,(1,(1,(1,(1,(0,1)))))))
+     | xbf => (1,(1,(1,(1,(1,(1,(0,1)))))))
+     | xc0 => (0,(0,(0,(0,(0,(0,(1,1)))))))
+     | xc1 => (1,(0,(0,(0,(0,(0,(1,1)))))))
+     | xc2 => (0,(1,(0,(0,(0,(0,(1,1)))))))
+     | xc3 => (1,(1,(0,(0,(0,(0,(1,1)))))))
+     | xc4 => (0,(0,(1,(0,(0,(0,(1,1)))))))
+     | xc5 => (1,(0,(1,(0,(0,(0,(1,1)))))))
+     | xc6 => (0,(1,(1,(0,(0,(0,(1,1)))))))
+     | xc7 => (1,(1,(1,(0,(0,(0,(1,1)))))))
+     | xc8 => (0,(0,(0,(1,(0,(0,(1,1)))))))
+     | xc9 => (1,(0,(0,(1,(0,(0,(1,1)))))))
+     | xca => (0,(1,(0,(1,(0,(0,(1,1)))))))
+     | xcb => (1,(1,(0,(1,(0,(0,(1,1)))))))
+     | xcc => (0,(0,(1,(1,(0,(0,(1,1)))))))
+     | xcd => (1,(0,(1,(1,(0,(0,(1,1)))))))
+     | xce => (0,(1,(1,(1,(0,(0,(1,1)))))))
+     | xcf => (1,(1,(1,(1,(0,(0,(1,1)))))))
+     | xd0 => (0,(0,(0,(0,(1,(0,(1,1)))))))
+     | xd1 => (1,(0,(0,(0,(1,(0,(1,1)))))))
+     | xd2 => (0,(1,(0,(0,(1,(0,(1,1)))))))
+     | xd3 => (1,(1,(0,(0,(1,(0,(1,1)))))))
+     | xd4 => (0,(0,(1,(0,(1,(0,(1,1)))))))
+     | xd5 => (1,(0,(1,(0,(1,(0,(1,1)))))))
+     | xd6 => (0,(1,(1,(0,(1,(0,(1,1)))))))
+     | xd7 => (1,(1,(1,(0,(1,(0,(1,1)))))))
+     | xd8 => (0,(0,(0,(1,(1,(0,(1,1)))))))
+     | xd9 => (1,(0,(0,(1,(1,(0,(1,1)))))))
+     | xda => (0,(1,(0,(1,(1,(0,(1,1)))))))
+     | xdb => (1,(1,(0,(1,(1,(0,(1,1)))))))
+     | xdc => (0,(0,(1,(1,(1,(0,(1,1)))))))
+     | xdd => (1,(0,(1,(1,(1,(0,(1,1)))))))
+     | xde => (0,(1,(1,(1,(1,(0,(1,1)))))))
+     | xdf => (1,(1,(1,(1,(1,(0,(1,1)))))))
+     | xe0 => (0,(0,(0,(0,(0,(1,(1,1)))))))
+     | xe1 => (1,(0,(0,(0,(0,(1,(1,1)))))))
+     | xe2 => (0,(1,(0,(0,(0,(1,(1,1)))))))
+     | xe3 => (1,(1,(0,(0,(0,(1,(1,1)))))))
+     | xe4 => (0,(0,(1,(0,(0,(1,(1,1)))))))
+     | xe5 => (1,(0,(1,(0,(0,(1,(1,1)))))))
+     | xe6 => (0,(1,(1,(0,(0,(1,(1,1)))))))
+     | xe7 => (1,(1,(1,(0,(0,(1,(1,1)))))))
+     | xe8 => (0,(0,(0,(1,(0,(1,(1,1)))))))
+     | xe9 => (1,(0,(0,(1,(0,(1,(1,1)))))))
+     | xea => (0,(1,(0,(1,(0,(1,(1,1)))))))
+     | xeb => (1,(1,(0,(1,(0,(1,(1,1)))))))
+     | xec => (0,(0,(1,(1,(0,(1,(1,1)))))))
+     | xed => (1,(0,(1,(1,(0,(1,(1,1)))))))
+     | xee => (0,(1,(1,(1,(0,(1,(1,1)))))))
+     | xef => (1,(1,(1,(1,(0,(1,(1,1)))))))
+     | xf0 => (0,(0,(0,(0,(1,(1,(1,1)))))))
+     | xf1 => (1,(0,(0,(0,(1,(1,(1,1)))))))
+     | xf2 => (0,(1,(0,(0,(1,(1,(1,1)))))))
+     | xf3 => (1,(1,(0,(0,(1,(1,(1,1)))))))
+     | xf4 => (0,(0,(1,(0,(1,(1,(1,1)))))))
+     | xf5 => (1,(0,(1,(0,(1,(1,(1,1)))))))
+     | xf6 => (0,(1,(1,(0,(1,(1,(1,1)))))))
+     | xf7 => (1,(1,(1,(0,(1,(1,(1,1)))))))
+     | xf8 => (0,(0,(0,(1,(1,(1,(1,1)))))))
+     | xf9 => (1,(0,(0,(1,(1,(1,(1,1)))))))
+     | xfa => (0,(1,(0,(1,(1,(1,(1,1)))))))
+     | xfb => (1,(1,(0,(1,(1,(1,(1,1)))))))
+     | xfc => (0,(0,(1,(1,(1,(1,(1,1)))))))
+     | xfd => (1,(0,(1,(1,(1,(1,(1,1)))))))
+     | xfe => (0,(1,(1,(1,(1,(1,(1,1)))))))
+     | xff => (1,(1,(1,(1,(1,(1,(1,1)))))))
+     end.
+
+Lemma of_bits_to_bits (b : byte) : of_bits (to_bits b) = b.
+Proof. destruct b; exact eq_refl. Qed.
+
+Lemma to_bits_of_bits (b : _) : to_bits (of_bits b) = b.
+Proof.
+  repeat match goal with
+         | p : prod _ _ |- _ => destruct p
+         | b : bool |- _ => destruct b
+         end;
+    exact eq_refl.
+Qed.
+
+Definition byte_of_byte (b : byte) : byte := b.
+
+Module Export ByteSyntaxNotations.
+  String Notation byte byte_of_byte byte_of_byte : byte_scope.
+End ByteSyntaxNotations.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 6d98bcb34a..5e29f854e8 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -13,6 +13,7 @@ Require Export Logic.
 Require Export Logic_Type.
 Require Export Datatypes.
 Require Export Specif.
+Require Coq.Init.Byte.
 Require Coq.Init.Decimal.
 Require Coq.Init.Nat.
 Require Export Peano.
@@ -26,6 +27,7 @@ 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 decimal numbers *)
 Arguments Nat.of_uint d%dec_uint_scope.
@@ -38,5 +40,8 @@ Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int
 (* Parsing / printing of [nat] numbers *)
 Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5000).
 
+(* Printing/Parsing of bytes *)
+Export Byte.ByteSyntaxNotations.
+
 (* Default substrings not considered by queries like SearchAbout *)
 Add Search Blacklist "_subproof" "_subterm" "Private_".
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index b7c1eaa788..6a0c5f066e 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -12,7 +12,7 @@
 (** Contributed by Laurent Théry (INRIA);
     Adapted to Coq V8 by the Coq Development Team *)
 
-Require Import Bool BinPos BinNat PeanoNat Nnat.
+Require Import Bool BinPos BinNat PeanoNat Nnat Coq.Strings.Byte.
 
 (** * Definition of ascii characters *)
 
@@ -20,10 +20,7 @@ Require Import Bool BinPos BinNat PeanoNat Nnat.
 
 Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).
 
-Register Ascii as plugins.syntax.Ascii.
-
 Declare Scope char_scope.
-Module Export AsciiSyntax. Declare ML Module "ascii_syntax_plugin". End AsciiSyntax.
 Delimit Scope char_scope with char.
 Bind Scope char_scope with ascii.
 
@@ -140,6 +137,12 @@ do 8 (destruct p; [ | | intros; vm_compute; reflexivity ]);
  intro H; vm_compute in H; destruct p; discriminate.
 Qed.
 
+Theorem N_ascii_bounded :
+  forall a : ascii, (N_of_ascii a < 256)%N.
+Proof.
+  destruct a as [[|][|][|][|][|][|][|][|]]; vm_compute; reflexivity.
+Qed.
+
 Theorem ascii_nat_embedding :
   forall a : ascii, ascii_of_nat (nat_of_ascii a) = a.
 Proof.
@@ -158,6 +161,15 @@ Proof.
  now apply Nat.compare_lt_iff.
 Qed.
 
+Theorem nat_ascii_bounded :
+  forall a : ascii, nat_of_ascii a < 256.
+Proof.
+  intro a; unfold nat_of_ascii.
+  change 256 with (N.to_nat 256).
+  rewrite <- Nat.compare_lt_iff, <- N2Nat.inj_compare, N.compare_lt_iff.
+  apply N_ascii_bounded.
+Qed.
+
 
 (** * Concrete syntax *)
 
@@ -175,7 +187,53 @@ Qed.
   stand-alone utf8 characters so that only the notation "nnn" is
   available for them (unless your terminal is able to represent them,
   which is typically not the case in coqide).
-*)
+ *)
+
+Definition ascii_of_byte (b : byte) : ascii
+  := let '(b0, (b1, (b2, (b3, (b4, (b5, (b6, b7))))))) := Byte.to_bits b in
+     Ascii b0 b1 b2 b3 b4 b5 b6 b7.
+
+Definition byte_of_ascii (a : ascii) : byte
+  := let (b0, b1, b2, b3, b4, b5, b6, b7) := a in
+     Byte.of_bits (b0, (b1, (b2, (b3, (b4, (b5, (b6, b7))))))).
+
+Lemma ascii_of_byte_of_ascii x : ascii_of_byte (byte_of_ascii x) = x.
+Proof.
+  cbv [ascii_of_byte byte_of_ascii].
+  destruct x; rewrite to_bits_of_bits; reflexivity.
+Qed.
+
+Lemma byte_of_ascii_of_byte x : byte_of_ascii (ascii_of_byte x) = x.
+Proof.
+  cbv [ascii_of_byte byte_of_ascii].
+  repeat match goal with
+         | [ |- context[match ?x with pair _ _ => _ end] ]
+           => rewrite (surjective_pairing x)
+         | [ |- context[(fst ?x, snd ?x)] ]
+           => rewrite <- (surjective_pairing x)
+         end.
+  rewrite of_bits_to_bits; reflexivity.
+Qed.
+
+Lemma ascii_of_byte_via_N x : ascii_of_byte x = ascii_of_N (Byte.to_N x).
+Proof. destruct x; reflexivity. Qed.
+
+Lemma ascii_of_byte_via_nat x : ascii_of_byte x = ascii_of_nat (Byte.to_nat x).
+Proof. destruct x; reflexivity. Qed.
+
+Lemma byte_of_ascii_via_N x : Some (byte_of_ascii x) = Byte.of_N (N_of_ascii x).
+Proof.
+  rewrite <- (ascii_of_byte_of_ascii x); destruct (byte_of_ascii x); reflexivity.
+Qed.
+
+Lemma byte_of_ascii_via_nat x : Some (byte_of_ascii x) = Byte.of_nat (nat_of_ascii x).
+Proof.
+  rewrite <- (ascii_of_byte_of_ascii x); destruct (byte_of_ascii x); reflexivity.
+Qed.
+
+Module Export AsciiSyntax.
+  String Notation ascii ascii_of_byte byte_of_ascii : char_scope.
+End AsciiSyntax.
 
 Local Open Scope char_scope.
 
diff --git a/theories/Strings/Byte.v b/theories/Strings/Byte.v
new file mode 100644
index 0000000000..2759ea60cb
--- /dev/null
+++ b/theories/Strings/Byte.v
@@ -0,0 +1,1214 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+Require Import Coq.Arith.EqNat.
+Require Import Coq.NArith.BinNat.
+Require Import Coq.NArith.Nnat.
+Require Export Coq.Init.Byte.
+
+Local Set Implicit Arguments.
+
+Definition eqb (a b : byte) : bool
+  := let '(a0, (a1, (a2, (a3, (a4, (a5, (a6, a7))))))) := to_bits a in
+     let '(b0, (b1, (b2, (b3, (b4, (b5, (b6, b7))))))) := to_bits b in
+     (Bool.eqb a0 b0 && Bool.eqb a1 b1 && Bool.eqb a2 b2 && Bool.eqb a3 b3 &&
+          Bool.eqb a4 b4 && Bool.eqb a5 b5 && Bool.eqb a6 b6 && Bool.eqb a7 b7)%bool.
+
+Module Export ByteNotations.
+  Export ByteSyntaxNotations.
+  Infix "=?" := eqb (at level 70) : byte_scope.
+End ByteNotations.
+
+Lemma byte_dec_lb x y : x = y -> eqb x y = true.
+Proof. intro; subst y; destruct x; reflexivity. Defined.
+
+Lemma byte_dec_bl x y (H : eqb x y = true) : x = y.
+Proof.
+  rewrite <- (of_bits_to_bits x), <- (of_bits_to_bits y).
+  cbv [eqb] in H; revert H.
+  generalize (to_bits x) (to_bits y); clear x y; intros x y H.
+  repeat match goal with
+         | [ H : and _ _ |- _ ] => destruct H
+         | [ H : prod _ _ |- _ ] => destruct H
+         | [ H : context[andb _ _ = true] |- _ ] => rewrite Bool.andb_true_iff in H
+         | [ H : context[Bool.eqb _ _ = true] |- _ ] => rewrite Bool.eqb_true_iff in H
+         | _ => progress subst
+         | _ => reflexivity
+         end.
+Qed.
+
+Lemma eqb_false x y : eqb x y = false -> x <> y.
+Proof. intros H H'; pose proof (byte_dec_lb H'); congruence. Qed.
+
+Definition byte_eq_dec (x y : byte) : {x = y} + {x <> y}
+  := (if eqb x y as beq return eqb x y = beq -> _
+      then fun pf => left (byte_dec_bl x y pf)
+      else fun pf => right (eqb_false pf))
+       eq_refl.
+
+Section nat.
+  Definition to_nat (x : byte) : nat
+    := match x with
+       | x00 => 0
+       | x01 => 1
+       | x02 => 2
+       | x03 => 3
+       | x04 => 4
+       | x05 => 5
+       | x06 => 6
+       | x07 => 7
+       | x08 => 8
+       | x09 => 9
+       | x0a => 10
+       | x0b => 11
+       | x0c => 12
+       | x0d => 13
+       | x0e => 14
+       | x0f => 15
+       | x10 => 16
+       | x11 => 17
+       | x12 => 18
+       | x13 => 19
+       | x14 => 20
+       | x15 => 21
+       | x16 => 22
+       | x17 => 23
+       | x18 => 24
+       | x19 => 25
+       | x1a => 26
+       | x1b => 27
+       | x1c => 28
+       | x1d => 29
+       | x1e => 30
+       | x1f => 31
+       | x20 => 32
+       | x21 => 33
+       | x22 => 34
+       | x23 => 35
+       | x24 => 36
+       | x25 => 37
+       | x26 => 38
+       | x27 => 39
+       | x28 => 40
+       | x29 => 41
+       | x2a => 42
+       | x2b => 43
+       | x2c => 44
+       | x2d => 45
+       | x2e => 46
+       | x2f => 47
+       | x30 => 48
+       | x31 => 49
+       | x32 => 50
+       | x33 => 51
+       | x34 => 52
+       | x35 => 53
+       | x36 => 54
+       | x37 => 55
+       | x38 => 56
+       | x39 => 57
+       | x3a => 58
+       | x3b => 59
+       | x3c => 60
+       | x3d => 61
+       | x3e => 62
+       | x3f => 63
+       | x40 => 64
+       | x41 => 65
+       | x42 => 66
+       | x43 => 67
+       | x44 => 68
+       | x45 => 69
+       | x46 => 70
+       | x47 => 71
+       | x48 => 72
+       | x49 => 73
+       | x4a => 74
+       | x4b => 75
+       | x4c => 76
+       | x4d => 77
+       | x4e => 78
+       | x4f => 79
+       | x50 => 80
+       | x51 => 81
+       | x52 => 82
+       | x53 => 83
+       | x54 => 84
+       | x55 => 85
+       | x56 => 86
+       | x57 => 87
+       | x58 => 88
+       | x59 => 89
+       | x5a => 90
+       | x5b => 91
+       | x5c => 92
+       | x5d => 93
+       | x5e => 94
+       | x5f => 95
+       | x60 => 96
+       | x61 => 97
+       | x62 => 98
+       | x63 => 99
+       | x64 => 100
+       | x65 => 101
+       | x66 => 102
+       | x67 => 103
+       | x68 => 104
+       | x69 => 105
+       | x6a => 106
+       | x6b => 107
+       | x6c => 108
+       | x6d => 109
+       | x6e => 110
+       | x6f => 111
+       | x70 => 112
+       | x71 => 113
+       | x72 => 114
+       | x73 => 115
+       | x74 => 116
+       | x75 => 117
+       | x76 => 118
+       | x77 => 119
+       | x78 => 120
+       | x79 => 121
+       | x7a => 122
+       | x7b => 123
+       | x7c => 124
+       | x7d => 125
+       | x7e => 126
+       | x7f => 127
+       | x80 => 128
+       | x81 => 129
+       | x82 => 130
+       | x83 => 131
+       | x84 => 132
+       | x85 => 133
+       | x86 => 134
+       | x87 => 135
+       | x88 => 136
+       | x89 => 137
+       | x8a => 138
+       | x8b => 139
+       | x8c => 140
+       | x8d => 141
+       | x8e => 142
+       | x8f => 143
+       | x90 => 144
+       | x91 => 145
+       | x92 => 146
+       | x93 => 147
+       | x94 => 148
+       | x95 => 149
+       | x96 => 150
+       | x97 => 151
+       | x98 => 152
+       | x99 => 153
+       | x9a => 154
+       | x9b => 155
+       | x9c => 156
+       | x9d => 157
+       | x9e => 158
+       | x9f => 159
+       | xa0 => 160
+       | xa1 => 161
+       | xa2 => 162
+       | xa3 => 163
+       | xa4 => 164
+       | xa5 => 165
+       | xa6 => 166
+       | xa7 => 167
+       | xa8 => 168
+       | xa9 => 169
+       | xaa => 170
+       | xab => 171
+       | xac => 172
+       | xad => 173
+       | xae => 174
+       | xaf => 175
+       | xb0 => 176
+       | xb1 => 177
+       | xb2 => 178
+       | xb3 => 179
+       | xb4 => 180
+       | xb5 => 181
+       | xb6 => 182
+       | xb7 => 183
+       | xb8 => 184
+       | xb9 => 185
+       | xba => 186
+       | xbb => 187
+       | xbc => 188
+       | xbd => 189
+       | xbe => 190
+       | xbf => 191
+       | xc0 => 192
+       | xc1 => 193
+       | xc2 => 194
+       | xc3 => 195
+       | xc4 => 196
+       | xc5 => 197
+       | xc6 => 198
+       | xc7 => 199
+       | xc8 => 200
+       | xc9 => 201
+       | xca => 202
+       | xcb => 203
+       | xcc => 204
+       | xcd => 205
+       | xce => 206
+       | xcf => 207
+       | xd0 => 208
+       | xd1 => 209
+       | xd2 => 210
+       | xd3 => 211
+       | xd4 => 212
+       | xd5 => 213
+       | xd6 => 214
+       | xd7 => 215
+       | xd8 => 216
+       | xd9 => 217
+       | xda => 218
+       | xdb => 219
+       | xdc => 220
+       | xdd => 221
+       | xde => 222
+       | xdf => 223
+       | xe0 => 224
+       | xe1 => 225
+       | xe2 => 226
+       | xe3 => 227
+       | xe4 => 228
+       | xe5 => 229
+       | xe6 => 230
+       | xe7 => 231
+       | xe8 => 232
+       | xe9 => 233
+       | xea => 234
+       | xeb => 235
+       | xec => 236
+       | xed => 237
+       | xee => 238
+       | xef => 239
+       | xf0 => 240
+       | xf1 => 241
+       | xf2 => 242
+       | xf3 => 243
+       | xf4 => 244
+       | xf5 => 245
+       | xf6 => 246
+       | xf7 => 247
+       | xf8 => 248
+       | xf9 => 249
+       | xfa => 250
+       | xfb => 251
+       | xfc => 252
+       | xfd => 253
+       | xfe => 254
+       | xff => 255
+       end.
+
+  Definition of_nat (x : nat) : option byte
+    := match x with
+       | 0 => Some x00
+       | 1 => Some x01
+       | 2 => Some x02
+       | 3 => Some x03
+       | 4 => Some x04
+       | 5 => Some x05
+       | 6 => Some x06
+       | 7 => Some x07
+       | 8 => Some x08
+       | 9 => Some x09
+       | 10 => Some x0a
+       | 11 => Some x0b
+       | 12 => Some x0c
+       | 13 => Some x0d
+       | 14 => Some x0e
+       | 15 => Some x0f
+       | 16 => Some x10
+       | 17 => Some x11
+       | 18 => Some x12
+       | 19 => Some x13
+       | 20 => Some x14
+       | 21 => Some x15
+       | 22 => Some x16
+       | 23 => Some x17
+       | 24 => Some x18
+       | 25 => Some x19
+       | 26 => Some x1a
+       | 27 => Some x1b
+       | 28 => Some x1c
+       | 29 => Some x1d
+       | 30 => Some x1e
+       | 31 => Some x1f
+       | 32 => Some x20
+       | 33 => Some x21
+       | 34 => Some x22
+       | 35 => Some x23
+       | 36 => Some x24
+       | 37 => Some x25
+       | 38 => Some x26
+       | 39 => Some x27
+       | 40 => Some x28
+       | 41 => Some x29
+       | 42 => Some x2a
+       | 43 => Some x2b
+       | 44 => Some x2c
+       | 45 => Some x2d
+       | 46 => Some x2e
+       | 47 => Some x2f
+       | 48 => Some x30
+       | 49 => Some x31
+       | 50 => Some x32
+       | 51 => Some x33
+       | 52 => Some x34
+       | 53 => Some x35
+       | 54 => Some x36
+       | 55 => Some x37
+       | 56 => Some x38
+       | 57 => Some x39
+       | 58 => Some x3a
+       | 59 => Some x3b
+       | 60 => Some x3c
+       | 61 => Some x3d
+       | 62 => Some x3e
+       | 63 => Some x3f
+       | 64 => Some x40
+       | 65 => Some x41
+       | 66 => Some x42
+       | 67 => Some x43
+       | 68 => Some x44
+       | 69 => Some x45
+       | 70 => Some x46
+       | 71 => Some x47
+       | 72 => Some x48
+       | 73 => Some x49
+       | 74 => Some x4a
+       | 75 => Some x4b
+       | 76 => Some x4c
+       | 77 => Some x4d
+       | 78 => Some x4e
+       | 79 => Some x4f
+       | 80 => Some x50
+       | 81 => Some x51
+       | 82 => Some x52
+       | 83 => Some x53
+       | 84 => Some x54
+       | 85 => Some x55
+       | 86 => Some x56
+       | 87 => Some x57
+       | 88 => Some x58
+       | 89 => Some x59
+       | 90 => Some x5a
+       | 91 => Some x5b
+       | 92 => Some x5c
+       | 93 => Some x5d
+       | 94 => Some x5e
+       | 95 => Some x5f
+       | 96 => Some x60
+       | 97 => Some x61
+       | 98 => Some x62
+       | 99 => Some x63
+       | 100 => Some x64
+       | 101 => Some x65
+       | 102 => Some x66
+       | 103 => Some x67
+       | 104 => Some x68
+       | 105 => Some x69
+       | 106 => Some x6a
+       | 107 => Some x6b
+       | 108 => Some x6c
+       | 109 => Some x6d
+       | 110 => Some x6e
+       | 111 => Some x6f
+       | 112 => Some x70
+       | 113 => Some x71
+       | 114 => Some x72
+       | 115 => Some x73
+       | 116 => Some x74
+       | 117 => Some x75
+       | 118 => Some x76
+       | 119 => Some x77
+       | 120 => Some x78
+       | 121 => Some x79
+       | 122 => Some x7a
+       | 123 => Some x7b
+       | 124 => Some x7c
+       | 125 => Some x7d
+       | 126 => Some x7e
+       | 127 => Some x7f
+       | 128 => Some x80
+       | 129 => Some x81
+       | 130 => Some x82
+       | 131 => Some x83
+       | 132 => Some x84
+       | 133 => Some x85
+       | 134 => Some x86
+       | 135 => Some x87
+       | 136 => Some x88
+       | 137 => Some x89
+       | 138 => Some x8a
+       | 139 => Some x8b
+       | 140 => Some x8c
+       | 141 => Some x8d
+       | 142 => Some x8e
+       | 143 => Some x8f
+       | 144 => Some x90
+       | 145 => Some x91
+       | 146 => Some x92
+       | 147 => Some x93
+       | 148 => Some x94
+       | 149 => Some x95
+       | 150 => Some x96
+       | 151 => Some x97
+       | 152 => Some x98
+       | 153 => Some x99
+       | 154 => Some x9a
+       | 155 => Some x9b
+       | 156 => Some x9c
+       | 157 => Some x9d
+       | 158 => Some x9e
+       | 159 => Some x9f
+       | 160 => Some xa0
+       | 161 => Some xa1
+       | 162 => Some xa2
+       | 163 => Some xa3
+       | 164 => Some xa4
+       | 165 => Some xa5
+       | 166 => Some xa6
+       | 167 => Some xa7
+       | 168 => Some xa8
+       | 169 => Some xa9
+       | 170 => Some xaa
+       | 171 => Some xab
+       | 172 => Some xac
+       | 173 => Some xad
+       | 174 => Some xae
+       | 175 => Some xaf
+       | 176 => Some xb0
+       | 177 => Some xb1
+       | 178 => Some xb2
+       | 179 => Some xb3
+       | 180 => Some xb4
+       | 181 => Some xb5
+       | 182 => Some xb6
+       | 183 => Some xb7
+       | 184 => Some xb8
+       | 185 => Some xb9
+       | 186 => Some xba
+       | 187 => Some xbb
+       | 188 => Some xbc
+       | 189 => Some xbd
+       | 190 => Some xbe
+       | 191 => Some xbf
+       | 192 => Some xc0
+       | 193 => Some xc1
+       | 194 => Some xc2
+       | 195 => Some xc3
+       | 196 => Some xc4
+       | 197 => Some xc5
+       | 198 => Some xc6
+       | 199 => Some xc7
+       | 200 => Some xc8
+       | 201 => Some xc9
+       | 202 => Some xca
+       | 203 => Some xcb
+       | 204 => Some xcc
+       | 205 => Some xcd
+       | 206 => Some xce
+       | 207 => Some xcf
+       | 208 => Some xd0
+       | 209 => Some xd1
+       | 210 => Some xd2
+       | 211 => Some xd3
+       | 212 => Some xd4
+       | 213 => Some xd5
+       | 214 => Some xd6
+       | 215 => Some xd7
+       | 216 => Some xd8
+       | 217 => Some xd9
+       | 218 => Some xda
+       | 219 => Some xdb
+       | 220 => Some xdc
+       | 221 => Some xdd
+       | 222 => Some xde
+       | 223 => Some xdf
+       | 224 => Some xe0
+       | 225 => Some xe1
+       | 226 => Some xe2
+       | 227 => Some xe3
+       | 228 => Some xe4
+       | 229 => Some xe5
+       | 230 => Some xe6
+       | 231 => Some xe7
+       | 232 => Some xe8
+       | 233 => Some xe9
+       | 234 => Some xea
+       | 235 => Some xeb
+       | 236 => Some xec
+       | 237 => Some xed
+       | 238 => Some xee
+       | 239 => Some xef
+       | 240 => Some xf0
+       | 241 => Some xf1
+       | 242 => Some xf2
+       | 243 => Some xf3
+       | 244 => Some xf4
+       | 245 => Some xf5
+       | 246 => Some xf6
+       | 247 => Some xf7
+       | 248 => Some xf8
+       | 249 => Some xf9
+       | 250 => Some xfa
+       | 251 => Some xfb
+       | 252 => Some xfc
+       | 253 => Some xfd
+       | 254 => Some xfe
+       | 255 => Some xff
+       | _ => None
+       end.
+
+  Lemma of_to_nat x : of_nat (to_nat x) = Some x.
+  Proof. destruct x; reflexivity. Qed.
+
+  Lemma to_of_nat x y : of_nat x = Some y -> to_nat y = x.
+  Proof.
+    do 256 try destruct x as [|x]; cbv [of_nat]; intro.
+    all: repeat match goal with
+                | _ => reflexivity
+                | _ => progress subst
+                | [ H : Some ?a = Some ?b |- _ ] => assert (a = b) by refine match H with eq_refl => eq_refl end; clear H
+                | [ H : None = Some _ |- _ ] => solve [ inversion H ]
+                end.
+  Qed.
+
+  Lemma to_of_nat_iff x y : of_nat x = Some y <-> to_nat y = x.
+  Proof. split; intro; subst; (apply of_to_nat || apply to_of_nat); assumption. Qed.
+
+  Lemma to_of_nat_option_map x : option_map to_nat (of_nat x) = if Nat.leb x 255 then Some x else None.
+  Proof. do 256 try destruct x as [|x]; reflexivity. Qed.
+
+  Lemma to_nat_bounded x : to_nat x <= 255.
+  Proof.
+    generalize (to_of_nat_option_map (to_nat x)).
+    rewrite of_to_nat; cbn [option_map].
+    destruct (Nat.leb (to_nat x) 255) eqn:H; [ | congruence ].
+    rewrite (PeanoNat.Nat.leb_le (to_nat x) 255) in H.
+    intro; assumption.
+  Qed.
+
+  Lemma of_nat_None_iff x : of_nat x = None <-> 255 < x.
+  Proof.
+    generalize (to_of_nat_option_map x).
+    destruct (of_nat x), (Nat.leb x 255) eqn:H; cbn [option_map]; try congruence.
+    { rewrite PeanoNat.Nat.leb_le in H; split; [ congruence | ].
+      rewrite PeanoNat.Nat.lt_nge; intro H'; exfalso; apply H'; assumption. }
+    { rewrite PeanoNat.Nat.leb_nle in H; split; [ | reflexivity ].
+      rewrite PeanoNat.Nat.lt_nge; intro; assumption. }
+  Qed.
+End nat.
+
+Section N.
+  Local Open Scope N_scope.
+
+  Definition to_N (x : byte) : N
+    := match x with
+       | x00 => 0
+       | x01 => 1
+       | x02 => 2
+       | x03 => 3
+       | x04 => 4
+       | x05 => 5
+       | x06 => 6
+       | x07 => 7
+       | x08 => 8
+       | x09 => 9
+       | x0a => 10
+       | x0b => 11
+       | x0c => 12
+       | x0d => 13
+       | x0e => 14
+       | x0f => 15
+       | x10 => 16
+       | x11 => 17
+       | x12 => 18
+       | x13 => 19
+       | x14 => 20
+       | x15 => 21
+       | x16 => 22
+       | x17 => 23
+       | x18 => 24
+       | x19 => 25
+       | x1a => 26
+       | x1b => 27
+       | x1c => 28
+       | x1d => 29
+       | x1e => 30
+       | x1f => 31
+       | x20 => 32
+       | x21 => 33
+       | x22 => 34
+       | x23 => 35
+       | x24 => 36
+       | x25 => 37
+       | x26 => 38
+       | x27 => 39
+       | x28 => 40
+       | x29 => 41
+       | x2a => 42
+       | x2b => 43
+       | x2c => 44
+       | x2d => 45
+       | x2e => 46
+       | x2f => 47
+       | x30 => 48
+       | x31 => 49
+       | x32 => 50
+       | x33 => 51
+       | x34 => 52
+       | x35 => 53
+       | x36 => 54
+       | x37 => 55
+       | x38 => 56
+       | x39 => 57
+       | x3a => 58
+       | x3b => 59
+       | x3c => 60
+       | x3d => 61
+       | x3e => 62
+       | x3f => 63
+       | x40 => 64
+       | x41 => 65
+       | x42 => 66
+       | x43 => 67
+       | x44 => 68
+       | x45 => 69
+       | x46 => 70
+       | x47 => 71
+       | x48 => 72
+       | x49 => 73
+       | x4a => 74
+       | x4b => 75
+       | x4c => 76
+       | x4d => 77
+       | x4e => 78
+       | x4f => 79
+       | x50 => 80
+       | x51 => 81
+       | x52 => 82
+       | x53 => 83
+       | x54 => 84
+       | x55 => 85
+       | x56 => 86
+       | x57 => 87
+       | x58 => 88
+       | x59 => 89
+       | x5a => 90
+       | x5b => 91
+       | x5c => 92
+       | x5d => 93
+       | x5e => 94
+       | x5f => 95
+       | x60 => 96
+       | x61 => 97
+       | x62 => 98
+       | x63 => 99
+       | x64 => 100
+       | x65 => 101
+       | x66 => 102
+       | x67 => 103
+       | x68 => 104
+       | x69 => 105
+       | x6a => 106
+       | x6b => 107
+       | x6c => 108
+       | x6d => 109
+       | x6e => 110
+       | x6f => 111
+       | x70 => 112
+       | x71 => 113
+       | x72 => 114
+       | x73 => 115
+       | x74 => 116
+       | x75 => 117
+       | x76 => 118
+       | x77 => 119
+       | x78 => 120
+       | x79 => 121
+       | x7a => 122
+       | x7b => 123
+       | x7c => 124
+       | x7d => 125
+       | x7e => 126
+       | x7f => 127
+       | x80 => 128
+       | x81 => 129
+       | x82 => 130
+       | x83 => 131
+       | x84 => 132
+       | x85 => 133
+       | x86 => 134
+       | x87 => 135
+       | x88 => 136
+       | x89 => 137
+       | x8a => 138
+       | x8b => 139
+       | x8c => 140
+       | x8d => 141
+       | x8e => 142
+       | x8f => 143
+       | x90 => 144
+       | x91 => 145
+       | x92 => 146
+       | x93 => 147
+       | x94 => 148
+       | x95 => 149
+       | x96 => 150
+       | x97 => 151
+       | x98 => 152
+       | x99 => 153
+       | x9a => 154
+       | x9b => 155
+       | x9c => 156
+       | x9d => 157
+       | x9e => 158
+       | x9f => 159
+       | xa0 => 160
+       | xa1 => 161
+       | xa2 => 162
+       | xa3 => 163
+       | xa4 => 164
+       | xa5 => 165
+       | xa6 => 166
+       | xa7 => 167
+       | xa8 => 168
+       | xa9 => 169
+       | xaa => 170
+       | xab => 171
+       | xac => 172
+       | xad => 173
+       | xae => 174
+       | xaf => 175
+       | xb0 => 176
+       | xb1 => 177
+       | xb2 => 178
+       | xb3 => 179
+       | xb4 => 180
+       | xb5 => 181
+       | xb6 => 182
+       | xb7 => 183
+       | xb8 => 184
+       | xb9 => 185
+       | xba => 186
+       | xbb => 187
+       | xbc => 188
+       | xbd => 189
+       | xbe => 190
+       | xbf => 191
+       | xc0 => 192
+       | xc1 => 193
+       | xc2 => 194
+       | xc3 => 195
+       | xc4 => 196
+       | xc5 => 197
+       | xc6 => 198
+       | xc7 => 199
+       | xc8 => 200
+       | xc9 => 201
+       | xca => 202
+       | xcb => 203
+       | xcc => 204
+       | xcd => 205
+       | xce => 206
+       | xcf => 207
+       | xd0 => 208
+       | xd1 => 209
+       | xd2 => 210
+       | xd3 => 211
+       | xd4 => 212
+       | xd5 => 213
+       | xd6 => 214
+       | xd7 => 215
+       | xd8 => 216
+       | xd9 => 217
+       | xda => 218
+       | xdb => 219
+       | xdc => 220
+       | xdd => 221
+       | xde => 222
+       | xdf => 223
+       | xe0 => 224
+       | xe1 => 225
+       | xe2 => 226
+       | xe3 => 227
+       | xe4 => 228
+       | xe5 => 229
+       | xe6 => 230
+       | xe7 => 231
+       | xe8 => 232
+       | xe9 => 233
+       | xea => 234
+       | xeb => 235
+       | xec => 236
+       | xed => 237
+       | xee => 238
+       | xef => 239
+       | xf0 => 240
+       | xf1 => 241
+       | xf2 => 242
+       | xf3 => 243
+       | xf4 => 244
+       | xf5 => 245
+       | xf6 => 246
+       | xf7 => 247
+       | xf8 => 248
+       | xf9 => 249
+       | xfa => 250
+       | xfb => 251
+       | xfc => 252
+       | xfd => 253
+       | xfe => 254
+       | xff => 255
+       end.
+
+  Definition of_N (x : N) : option byte
+    := match x with
+       | 0 => Some x00
+       | 1 => Some x01
+       | 2 => Some x02
+       | 3 => Some x03
+       | 4 => Some x04
+       | 5 => Some x05
+       | 6 => Some x06
+       | 7 => Some x07
+       | 8 => Some x08
+       | 9 => Some x09
+       | 10 => Some x0a
+       | 11 => Some x0b
+       | 12 => Some x0c
+       | 13 => Some x0d
+       | 14 => Some x0e
+       | 15 => Some x0f
+       | 16 => Some x10
+       | 17 => Some x11
+       | 18 => Some x12
+       | 19 => Some x13
+       | 20 => Some x14
+       | 21 => Some x15
+       | 22 => Some x16
+       | 23 => Some x17
+       | 24 => Some x18
+       | 25 => Some x19
+       | 26 => Some x1a
+       | 27 => Some x1b
+       | 28 => Some x1c
+       | 29 => Some x1d
+       | 30 => Some x1e
+       | 31 => Some x1f
+       | 32 => Some x20
+       | 33 => Some x21
+       | 34 => Some x22
+       | 35 => Some x23
+       | 36 => Some x24
+       | 37 => Some x25
+       | 38 => Some x26
+       | 39 => Some x27
+       | 40 => Some x28
+       | 41 => Some x29
+       | 42 => Some x2a
+       | 43 => Some x2b
+       | 44 => Some x2c
+       | 45 => Some x2d
+       | 46 => Some x2e
+       | 47 => Some x2f
+       | 48 => Some x30
+       | 49 => Some x31
+       | 50 => Some x32
+       | 51 => Some x33
+       | 52 => Some x34
+       | 53 => Some x35
+       | 54 => Some x36
+       | 55 => Some x37
+       | 56 => Some x38
+       | 57 => Some x39
+       | 58 => Some x3a
+       | 59 => Some x3b
+       | 60 => Some x3c
+       | 61 => Some x3d
+       | 62 => Some x3e
+       | 63 => Some x3f
+       | 64 => Some x40
+       | 65 => Some x41
+       | 66 => Some x42
+       | 67 => Some x43
+       | 68 => Some x44
+       | 69 => Some x45
+       | 70 => Some x46
+       | 71 => Some x47
+       | 72 => Some x48
+       | 73 => Some x49
+       | 74 => Some x4a
+       | 75 => Some x4b
+       | 76 => Some x4c
+       | 77 => Some x4d
+       | 78 => Some x4e
+       | 79 => Some x4f
+       | 80 => Some x50
+       | 81 => Some x51
+       | 82 => Some x52
+       | 83 => Some x53
+       | 84 => Some x54
+       | 85 => Some x55
+       | 86 => Some x56
+       | 87 => Some x57
+       | 88 => Some x58
+       | 89 => Some x59
+       | 90 => Some x5a
+       | 91 => Some x5b
+       | 92 => Some x5c
+       | 93 => Some x5d
+       | 94 => Some x5e
+       | 95 => Some x5f
+       | 96 => Some x60
+       | 97 => Some x61
+       | 98 => Some x62
+       | 99 => Some x63
+       | 100 => Some x64
+       | 101 => Some x65
+       | 102 => Some x66
+       | 103 => Some x67
+       | 104 => Some x68
+       | 105 => Some x69
+       | 106 => Some x6a
+       | 107 => Some x6b
+       | 108 => Some x6c
+       | 109 => Some x6d
+       | 110 => Some x6e
+       | 111 => Some x6f
+       | 112 => Some x70
+       | 113 => Some x71
+       | 114 => Some x72
+       | 115 => Some x73
+       | 116 => Some x74
+       | 117 => Some x75
+       | 118 => Some x76
+       | 119 => Some x77
+       | 120 => Some x78
+       | 121 => Some x79
+       | 122 => Some x7a
+       | 123 => Some x7b
+       | 124 => Some x7c
+       | 125 => Some x7d
+       | 126 => Some x7e
+       | 127 => Some x7f
+       | 128 => Some x80
+       | 129 => Some x81
+       | 130 => Some x82
+       | 131 => Some x83
+       | 132 => Some x84
+       | 133 => Some x85
+       | 134 => Some x86
+       | 135 => Some x87
+       | 136 => Some x88
+       | 137 => Some x89
+       | 138 => Some x8a
+       | 139 => Some x8b
+       | 140 => Some x8c
+       | 141 => Some x8d
+       | 142 => Some x8e
+       | 143 => Some x8f
+       | 144 => Some x90
+       | 145 => Some x91
+       | 146 => Some x92
+       | 147 => Some x93
+       | 148 => Some x94
+       | 149 => Some x95
+       | 150 => Some x96
+       | 151 => Some x97
+       | 152 => Some x98
+       | 153 => Some x99
+       | 154 => Some x9a
+       | 155 => Some x9b
+       | 156 => Some x9c
+       | 157 => Some x9d
+       | 158 => Some x9e
+       | 159 => Some x9f
+       | 160 => Some xa0
+       | 161 => Some xa1
+       | 162 => Some xa2
+       | 163 => Some xa3
+       | 164 => Some xa4
+       | 165 => Some xa5
+       | 166 => Some xa6
+       | 167 => Some xa7
+       | 168 => Some xa8
+       | 169 => Some xa9
+       | 170 => Some xaa
+       | 171 => Some xab
+       | 172 => Some xac
+       | 173 => Some xad
+       | 174 => Some xae
+       | 175 => Some xaf
+       | 176 => Some xb0
+       | 177 => Some xb1
+       | 178 => Some xb2
+       | 179 => Some xb3
+       | 180 => Some xb4
+       | 181 => Some xb5
+       | 182 => Some xb6
+       | 183 => Some xb7
+       | 184 => Some xb8
+       | 185 => Some xb9
+       | 186 => Some xba
+       | 187 => Some xbb
+       | 188 => Some xbc
+       | 189 => Some xbd
+       | 190 => Some xbe
+       | 191 => Some xbf
+       | 192 => Some xc0
+       | 193 => Some xc1
+       | 194 => Some xc2
+       | 195 => Some xc3
+       | 196 => Some xc4
+       | 197 => Some xc5
+       | 198 => Some xc6
+       | 199 => Some xc7
+       | 200 => Some xc8
+       | 201 => Some xc9
+       | 202 => Some xca
+       | 203 => Some xcb
+       | 204 => Some xcc
+       | 205 => Some xcd
+       | 206 => Some xce
+       | 207 => Some xcf
+       | 208 => Some xd0
+       | 209 => Some xd1
+       | 210 => Some xd2
+       | 211 => Some xd3
+       | 212 => Some xd4
+       | 213 => Some xd5
+       | 214 => Some xd6
+       | 215 => Some xd7
+       | 216 => Some xd8
+       | 217 => Some xd9
+       | 218 => Some xda
+       | 219 => Some xdb
+       | 220 => Some xdc
+       | 221 => Some xdd
+       | 222 => Some xde
+       | 223 => Some xdf
+       | 224 => Some xe0
+       | 225 => Some xe1
+       | 226 => Some xe2
+       | 227 => Some xe3
+       | 228 => Some xe4
+       | 229 => Some xe5
+       | 230 => Some xe6
+       | 231 => Some xe7
+       | 232 => Some xe8
+       | 233 => Some xe9
+       | 234 => Some xea
+       | 235 => Some xeb
+       | 236 => Some xec
+       | 237 => Some xed
+       | 238 => Some xee
+       | 239 => Some xef
+       | 240 => Some xf0
+       | 241 => Some xf1
+       | 242 => Some xf2
+       | 243 => Some xf3
+       | 244 => Some xf4
+       | 245 => Some xf5
+       | 246 => Some xf6
+       | 247 => Some xf7
+       | 248 => Some xf8
+       | 249 => Some xf9
+       | 250 => Some xfa
+       | 251 => Some xfb
+       | 252 => Some xfc
+       | 253 => Some xfd
+       | 254 => Some xfe
+       | 255 => Some xff
+       | _ => None
+       end.
+
+  Lemma of_to_N x : of_N (to_N x) = Some x.
+  Proof. destruct x; reflexivity. Qed.
+
+  Lemma to_of_N x y : of_N x = Some y -> to_N y = x.
+  Proof.
+    cbv [of_N];
+      repeat match goal with
+             | [ |- context[match ?x with _ => _ end] ] => is_var x; destruct x
+             | _ => intro
+             | _ => reflexivity
+             | _ => progress subst
+             | [ H : Some ?a = Some ?b |- _ ] => assert (a = b) by refine match H with eq_refl => eq_refl end; clear H
+             | [ H : None = Some _ |- _ ] => solve [ inversion H ]
+             end.
+  Qed.
+
+  Lemma to_of_N_iff x y : of_N x = Some y <-> to_N y = x.
+  Proof. split; intro; subst; (apply of_to_N || apply to_of_N); assumption. Qed.
+
+  Lemma to_of_N_option_map x : option_map to_N (of_N x) = if N.leb x 255 then Some x else None.
+  Proof.
+    cbv [of_N];
+      repeat match goal with
+             | [ |- context[match ?x with _ => _ end] ] => is_var x; destruct x
+             end;
+      reflexivity.
+  Qed.
+
+  Lemma to_N_bounded x : to_N x <= 255.
+  Proof.
+    generalize (to_of_N_option_map (to_N x)).
+    rewrite of_to_N; cbn [option_map].
+    destruct (N.leb (to_N x) 255) eqn:H; [ | congruence ].
+    rewrite (N.leb_le (to_N x) 255) in H.
+    intro; assumption.
+  Qed.
+
+  Lemma of_N_None_iff x : of_N x = None <-> 255 < x.
+  Proof.
+    generalize (to_of_N_option_map x).
+    destruct (of_N x), (N.leb x 255) eqn:H; cbn [option_map]; try congruence.
+    { rewrite N.leb_le in H; split; [ congruence | ].
+      rewrite N.lt_nge; intro H'; exfalso; apply H'; assumption. }
+    { rewrite N.leb_nle in H; split; [ | reflexivity ].
+      rewrite N.lt_nge; intro; assumption. }
+  Qed.
+
+  Lemma to_N_via_nat x : to_N x = N.of_nat (to_nat x).
+  Proof. destruct x; reflexivity. Qed.
+
+  Lemma to_nat_via_N x : to_nat x = N.to_nat (to_N x).
+  Proof. destruct x; reflexivity. Qed.
+
+  Lemma of_N_via_nat x : of_N x = of_nat (N.to_nat x).
+  Proof.
+    destruct (of_N x) as [b|] eqn:H1.
+    { rewrite to_of_N_iff in H1; subst.
+      destruct b; reflexivity. }
+    { rewrite of_N_None_iff, <- N.compare_lt_iff in H1.
+      symmetry; rewrite of_nat_None_iff, <- PeanoNat.Nat.compare_lt_iff.
+      rewrite Nat2N.inj_compare, N2Nat.id; assumption. }
+  Qed.
+
+  Lemma of_nat_via_N x : of_nat x = of_N (N.of_nat x).
+  Proof.
+    destruct (of_nat x) as [b|] eqn:H1.
+    { rewrite to_of_nat_iff in H1; subst.
+      destruct b; reflexivity. }
+    { rewrite of_nat_None_iff, <- PeanoNat.Nat.compare_lt_iff in H1.
+      symmetry; rewrite of_N_None_iff, <- N.compare_lt_iff.
+      rewrite N2Nat.inj_compare, Nat2N.id; assumption. }
+  Qed.
+End N.
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index a09d518892..08ccfac877 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -15,6 +15,7 @@
 Require Import Arith.
 Require Import Ascii.
 Require Import Bool.
+Require Import Coq.Strings.Byte.
 
 (** *** Definition of strings *)
 
@@ -25,7 +26,6 @@ Inductive string : Set :=
   | String : ascii -> string -> string.
 
 Declare Scope string_scope.
-Module Export StringSyntax. Declare ML Module "string_syntax_plugin". End StringSyntax.
 Delimit Scope string_scope with string.
 Bind Scope string_scope with string.
 Local Open Scope string_scope.
@@ -114,12 +114,12 @@ Theorem get_correct :
 Proof.
 intros s1; elim s1; simpl.
 intros s2; case s2; simpl; split; auto.
-intros H; generalize (H 0); intros H1; inversion H1.
+intros H; generalize (H O); intros H1; inversion H1.
 intros; discriminate.
 intros a s1' Rec s2; case s2; simpl; split; auto.
-intros H; generalize (H 0); intros H1; inversion H1.
+intros H; generalize (H O); intros H1; inversion H1.
 intros; discriminate.
-intros H; generalize (H 0); simpl; intros H1; inversion H1.
+intros H; generalize (H O); simpl; intros H1; inversion H1.
 case (Rec s).
 intros H0; rewrite H0; auto.
 intros n; exact (H (S n)).
@@ -150,7 +150,7 @@ Proof.
 intros s1; elim s1; simpl; auto.
 intros s2 n; rewrite plus_comm; simpl; auto.
 intros a s1' Rec s2 n; case n; simpl; auto.
-generalize (Rec s2 0); simpl; auto. intros.
+generalize (Rec s2 O); simpl; auto. intros.
 rewrite <- Plus.plus_Snm_nSm; auto.
 Qed.
 
@@ -162,9 +162,9 @@ Qed.
 
 Fixpoint substring (n m : nat) (s : string) : string :=
   match n, m, s with
-  | 0, 0, _ => EmptyString
-  | 0, S m', EmptyString => s
-  | 0, S m', String c s' => String c (substring 0 m' s')
+  | O, O, _ => EmptyString
+  | O, S m', EmptyString => s
+  | O, S m', String c s' => String c (substring 0 m' s')
   | S n', _, EmptyString => s
   | S n', _, String c s' => substring n' m s'
   end.
@@ -257,16 +257,16 @@ Qed.
 
 Fixpoint index (n : nat) (s1 s2 : string) : option nat :=
   match s2, n with
-  | EmptyString, 0 =>
+  | EmptyString, O =>
       match s1 with
-      | EmptyString => Some 0
+      | EmptyString => Some O
       | String a s1' => None
       end
   | EmptyString, S n' => None
-  | String b s2', 0 =>
-      if prefix s1 s2 then Some 0
+  | String b s2', O =>
+      if prefix s1 s2 then Some O
       else
-        match index 0 s1 s2' with
+        match index O s1 s2' with
         | Some n => Some (S n)
         | None => None
         end
@@ -300,8 +300,8 @@ generalize (prefix_correct s1 (String b s2'));
 intros H0 H; injection H as <-; auto.
 case H0; simpl; auto.
 case m; simpl; auto.
-case (index 0 s1 s2'); intros; discriminate.
-intros m'; generalize (Rec 0 m' s1); case (index 0 s1 s2'); auto.
+case (index O s1 s2'); intros; discriminate.
+intros m'; generalize (Rec O m' s1); case (index O s1 s2'); auto.
 intros x H H0 H1; apply H; injection H1; auto.
 intros; discriminate.
 intros n'; case m; simpl; auto.
@@ -335,7 +335,7 @@ intros H0 H; injection H as <-; auto.
 intros p H2 H3; inversion H3.
 case m; simpl; auto.
 case (index 0 s1 s2'); intros; discriminate.
-intros m'; generalize (Rec 0 m' s1); case (index 0 s1 s2'); auto.
+intros m'; generalize (Rec O m' s1); case (index 0 s1 s2'); auto.
 intros x H H0 H1 p; try case p; simpl; auto.
 intros H2 H3; red; intros H4; case H0.
 intros H5 H6; absurd (false = true); auto with bool.
@@ -383,7 +383,7 @@ intros H4 H5; absurd (false = true); auto with bool.
 case s1; simpl; auto.
 intros a s n0 H H0 H1 H2;
  change (substring n0 (length (String a s)) s2' <> String a s);
- apply (Rec 0); auto.
+ apply (Rec O); auto.
 generalize H0; case (index 0 (String a s) s2'); simpl; auto; intros;
  discriminate.
 apply Le.le_O_n.
@@ -423,9 +423,53 @@ Qed.
 Definition findex n s1 s2 :=
   match index n s1 s2 with
   | Some n => n
-  | None => 0
+  | None => O
   end.
 
+(** *** Conversion to/from [list ascii] and [list byte] *)
+
+Fixpoint string_of_list_ascii (s : list ascii) : string
+  := match s with
+     | nil => EmptyString
+     | cons ch s => String ch (string_of_list_ascii s)
+     end.
+
+Fixpoint list_ascii_of_string (s : string) : list ascii
+  := match s with
+     | EmptyString => nil
+     | String ch s => cons ch (list_ascii_of_string s)
+     end.
+
+Lemma string_of_list_ascii_of_string s : string_of_list_ascii (list_ascii_of_string s) = s.
+Proof.
+  induction s as [|? ? IHs]; [ reflexivity | cbn; apply f_equal, IHs ].
+Defined.
+
+Lemma list_ascii_of_string_of_list_ascii s : list_ascii_of_string (string_of_list_ascii s) = s.
+Proof.
+  induction s as [|? ? IHs]; [ reflexivity | cbn; apply f_equal, IHs ].
+Defined.
+
+Definition string_of_list_byte (s : list byte) : string
+  := string_of_list_ascii (List.map ascii_of_byte s).
+
+Definition list_byte_of_string (s : string) : list byte
+  := List.map byte_of_ascii (list_ascii_of_string s).
+
+Lemma string_of_list_byte_of_string s : string_of_list_byte (list_byte_of_string s) = s.
+Proof.
+  cbv [string_of_list_byte list_byte_of_string].
+  erewrite List.map_map, List.map_ext, List.map_id, string_of_list_ascii_of_string; [ reflexivity | intro ].
+  apply ascii_of_byte_of_ascii.
+Qed.
+
+Lemma list_byte_of_string_of_list_byte s : list_byte_of_string (string_of_list_byte s) = s.
+Proof.
+  cbv [string_of_list_byte list_byte_of_string].
+  erewrite list_ascii_of_string_of_list_ascii, List.map_map, List.map_ext, List.map_id; [ reflexivity | intro ].
+  apply byte_of_ascii_of_byte.
+Qed.
+
 (** *** Concrete syntax *)
 
 (**
@@ -438,7 +482,11 @@ Definition findex n s1 s2 :=
   part of a valid utf8 sequence of characters are not representable
   using the Coq string notation (use explicitly the String constructor
   with the ascii codes of the characters).
-*)
+ *)
+
+Module Export StringSyntax.
+  String Notation string string_of_list_byte list_byte_of_string : string_scope.
+End StringSyntax.
 
 Example HelloWorld := "	""Hello world!""
 ".