From 5e31d0be41febb6d5a54aa4a0d189b41c9bf1c2e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 8 Jun 2010 14:06:28 +0000
Subject: Fixed wrong spelling in a warning.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13092 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/notation.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index bfa86b50f2..31e242c1f3 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -151,7 +151,7 @@ let declare_delimiters scope key =
     | Some oldkey when oldkey = key -> ()
     | Some oldkey ->
 	Flags.if_verbose warning
-	  ("Overwritting previous delimiting key "^oldkey^" in scope "^scope);
+	  ("overwriting previous delimiting key "^oldkey^" in scope "^scope);
 	scope_map := Gmap.add scope newsc !scope_map
   end;
   try
-- 
cgit v1.2.3