From 0fb8601151a0e316554c95608de2ae4dbdac2ed3 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 2 Nov 2009 18:50:33 +0000
Subject: Remove various useless {struct} annotations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12458 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Strings/Ascii.v  | 2 +-
 theories/Strings/String.v | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'theories/Strings')

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
-- 
cgit v1.2.3