From 3c5ff2175d0711da2dca1259b953f308cd5d82ae Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Fri, 9 Oct 2020 16:38:52 -0700
Subject: Modify Strings/String.v to compile with -mangle-names

---
 theories/Strings/String.v | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index a468a4fe87..b792acc9f9 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -54,7 +54,8 @@ Infix "=?" := eqb : string_scope.
 
 Lemma eqb_spec s1 s2 : Bool.reflect (s1 = s2) (s1 =? s2)%string.
 Proof.
- revert s2. induction s1; destruct s2; try (constructor; easy); simpl.
+ revert s2. induction s1 as [|? s1 IHs1];
+  intro s2; destruct s2; try (constructor; easy); simpl.
  case Ascii.eqb_spec; simpl; [intros -> | constructor; now intros [= ]].
  case IHs1; [intros ->; now constructor | constructor; now intros [= ]].
 Qed.
@@ -117,7 +118,7 @@ intros s1; elim s1; simpl.
 intros s2; case s2; simpl; split; auto.
 intros H; generalize (H O); intros H1; inversion H1.
 intros; discriminate.
-intros a s1' Rec s2; case s2; simpl; split; auto.
+intros a s1' Rec s2; case s2 as [|? s]; simpl; split; auto.
 intros H; generalize (H O); intros H1; inversion H1.
 intros; discriminate.
 intros H; generalize (H O); simpl; intros H1; inversion H1.
@@ -249,7 +250,7 @@ intros b s2'; case (ascii_dec a b); simpl; auto.
 intros e; case (Rec s2'); intros H1 H2; split; intros H3; auto.
 rewrite e; rewrite H1; auto.
 apply H2; injection H3; auto.
-intros n; split; intros; try discriminate.
+intros n; split; intros H; try discriminate.
 case n; injection H; auto.
 Qed.
 
-- 
cgit v1.2.3