2 files changed, 4 insertions, 4 deletions
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 87d8e1350..1f90c06cf 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -59,7 +59,7 @@ Defined.
    looking at the last n bits, ie z mod 2^n *)
 
 Fixpoint ascii_of_pos_aux (res acc : ascii) (z : positive)
-  (n : nat) {struct n} : ascii :=
+  (n : nat) : ascii :=
   match n with
     | O => res
     | S n1 =>
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index 21c0a15e9..15f298218 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -38,7 +38,7 @@ Defined.
 
 Reserved Notation "x ++ y" (right associativity, at level 60).
 
-Fixpoint append (s1 s2 : string) {struct s1} : string :=
+Fixpoint append (s1 s2 : string) : string :=
   match s1 with
   | EmptyString => s2
   | String c s1' => String c (s1' ++ s2)
@@ -122,7 +122,7 @@ Qed.
     at position [n] and of length [m];
     if this does not make sense it returns [""] *)
 
-Fixpoint substring (n m : nat) (s : string) {struct s} : string :=
+Fixpoint substring (n m : nat) (s : string) : string :=
   match n, m, s with
   | 0, 0, _ => EmptyString
   | 0, S m', EmptyString => s
@@ -205,7 +205,7 @@ Qed.
 (** Test if, starting at position [n], [s1] occurs in [s2]; if
     so it returns the position *)
 
-Fixpoint index (n : nat) (s1 s2 : string) {struct s2} : option nat :=
+Fixpoint index (n : nat) (s1 s2 : string) : option nat :=
   match s2, n with
   | EmptyString, 0 =>
       match s1 with