From 5a3d6f1d2c193be514e610779b80829eef4fe4a8 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Fri, 9 Oct 2020 16:33:49 -0700
Subject: Modify Strings/Ascii.v to compile with -mangle-names

---
 theories/Strings/Ascii.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index c155395ecd..06b02ab211 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -128,28 +128,28 @@ Definition nat_of_ascii (a : ascii) : nat := N.to_nat (N_of_ascii a).
 Theorem ascii_N_embedding :
   forall a : ascii, ascii_of_N (N_of_ascii a) = a.
 Proof.
-  destruct a as [[|][|][|][|][|][|][|][|]]; vm_compute; reflexivity.
+  intro a; destruct a as [[|][|][|][|][|][|][|][|]]; vm_compute; reflexivity.
 Qed.
 
 Theorem N_ascii_embedding :
   forall n:N, (n < 256)%N -> N_of_ascii (ascii_of_N n) = n.
 Proof.
-destruct n.
+intro n; destruct n as [|p].
 reflexivity.
-do 8 (destruct p; [ | | intros; vm_compute; reflexivity ]);
+do 8 (destruct p as [p|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.
+  intro a; destruct a as [[|][|][|][|][|][|][|][|]]; vm_compute; reflexivity.
 Qed.
 
 Theorem ascii_nat_embedding :
   forall a : ascii, ascii_of_nat (nat_of_ascii a) = a.
 Proof.
-  destruct a as [[|][|][|][|][|][|][|][|]]; compute; reflexivity.
+  intro a; destruct a as [[|][|][|][|][|][|][|][|]]; compute; reflexivity.
 Qed.
 
 Theorem nat_ascii_embedding :
-- 
cgit v1.2.3