From c4370e5394cc9f678250150bd5bb407629b21913 Mon Sep 17 00:00:00 2001
From: xclerc
Date: Mon, 24 Feb 2014 11:07:21 +0100
Subject: Fix grammatical mistake in error message (bug #3238)

---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e765fa8cd6..5b5775d1a3 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1300,7 +1300,7 @@ let check_projection isproj nargs r =
       (try
 	let n = Recordops.find_projection_nparams ref + 1 in
 	if not (Int.equal nargs n) then
-	  user_err_loc (loc,"",str "Projection has not the right number of explicit parameters.");
+	  user_err_loc (loc,"",str "Projection does not have the right number of explicit parameters.");
       with Not_found ->
 	user_err_loc
 	(loc,"",pr_global_env Id.Set.empty ref ++ str " is not a registered projection."))
-- 
cgit v1.2.3