From e99804d987ac376a79e0769b809989388cc3a34a Mon Sep 17 00:00:00 2001
From: Robbert <gitlab-sws@robbertkrebbers.nl>
Date: Tue, 12 May 2020 19:32:51 +0200
Subject: [PATCH] Revert "Merge branch 'byte-countable' into 'master'"

This reverts merge request !155
---
 CHANGELOG.md       | 3 +--
 theories/strings.v | 4 ----
 2 files changed, 1 insertion(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3b982a91..3e873810 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -14,8 +14,7 @@ API-breaking change is listed.
   exported by the prelude. This is a breaking change if one only
   imports `list.v`, but not the prelude.
 - Rename `drop_insert` into `drop_insert_gt` and add `drop_insert_le`.
-- Added `Countable` instances for `Ascii.ascii` and `Byte.byte` from the Coq
-  standard library.
+- Added `Countable` instance for `Ascii.ascii`.
 - Make lemma `list_find_Some` more apply friendly.
 
 ## std++ 1.3 (released 2020-03-18)
diff --git a/theories/strings.v b/theories/strings.v
index 0f94448e..a9f2bcc5 100644
--- a/theories/strings.v
+++ b/theories/strings.v
@@ -1,5 +1,4 @@
 From Coq Require Import Ascii.
-From Coq Require Import Init.Byte.
 From Coq Require Export String.
 From stdpp Require Export list.
 From stdpp Require Import countable.
@@ -19,7 +18,6 @@ Arguments String.append : simpl never.
 
 (** * Decision of equality *)
 Instance ascii_eq_dec : EqDecision ascii := ascii_dec.
-Instance byte_eq_dec : EqDecision byte := Byte.byte_eq_dec.
 Instance string_eq_dec : EqDecision string.
 Proof. solve_decision. Defined.
 Instance string_app_inj : Inj (=) (=) (String.append s1).
@@ -121,5 +119,3 @@ Lemma ascii_of_to_digits a : ascii_of_digits (ascii_to_digits a) = a.
 Proof. by destruct a as [[][][][][][][][]]. Qed.
 Instance ascii_countable : Countable ascii :=
   inj_countable' ascii_to_digits ascii_of_digits ascii_of_to_digits.
-Instance byte_countable : Countable byte :=
-  inj_countable Byte.to_N Byte.of_N Byte.of_to_N.
-- 
GitLab