From 6f88442be8275361a7b68fd56d40976fdee9f4d5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 18 Nov 2015 15:58:17 +0100
Subject: Improve error message.

---
 tactics/tacinterp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 355745d970..d244129425 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -989,7 +989,7 @@ let interp_induction_arg ist gl arg =
           try sigma, (constr_of_id env id', NoBindings)
           with Not_found ->
             user_err_loc (loc, "interp_induction_arg",
-            pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared or a quantified hypothesis."))
+            pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis."))
       in
       try
         (** FIXME: should be moved to taccoerce *)
-- 
cgit v1.2.3