aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Strings
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-20 13:44:45 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-20 13:44:45 +0000
commit276a2b595e18c3176ed2250aa4966bc6e728620e (patch)
tree10663bede23242e04cc33eb632830363c04c11cb /theories/Strings
parentf3375ecf605d51d1f06c0af5e1f10a3e1923bd02 (diff)
typo in a comment
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11155 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Strings')
-rw-r--r--theories/Strings/String.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index 6826e0c51..59edf8187 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -225,7 +225,7 @@ Fixpoint index (n : nat) (s1 s2 : string) {struct s2} : option nat :=
end
end.
-(* Dirty trick to evaluate locally that prefix reduces itself *)
+(* Dirty trick to avoid locally that prefix reduces itself *)
Opaque prefix.
(** If the result of [index] is [Some m], [s1] in [s2] at position [m] *)