Merge PR #13173: Lint stdlib with -mangle-names #4

Reviewed-by: anton-trunov

2 files changed, 9 insertions, 8 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 :
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.