diff options
Diffstat (limited to 'theories/Strings')
-rw-r--r-- | theories/Strings/String.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 4057ba022..6826e0c51 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -110,8 +110,8 @@ Proof. intros s1; elim s1; simpl in |- *; auto. intros s2 n; rewrite plus_comm; simpl in |- *; auto. intros a s1' Rec s2 n; case n; simpl in |- *; auto. -generalize (Rec s2 0); simpl in |- *; auto. -intros n0; rewrite <- Plus.plus_Snm_nSm; auto. +generalize (Rec s2 0); simpl in |- *; auto. intros. +rewrite <- Plus.plus_Snm_nSm; auto. Qed. (** *** Substrings *) |