diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-02 18:50:33 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-02 18:50:33 +0000 |
commit | 0fb8601151a0e316554c95608de2ae4dbdac2ed3 (patch) | |
tree | eef149e1c23427c2bd4943cf72b3a276a3a82808 /theories/Strings/String.v | |
parent | d70800791ded96209c8f71e682f602201f93d56b (diff) |
Remove various useless {struct} annotations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12458 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Strings/String.v')
-rw-r--r-- | theories/Strings/String.v | 6 |
1 files changed, 3 insertions, 3 deletions
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 |