From 276a2b595e18c3176ed2250aa4966bc6e728620e Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 20 Jun 2008 13:44:45 +0000 Subject: typo in a comment git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11155 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Strings/String.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Strings') 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] *) -- cgit v1.2.3