From dc13be3390c7b1d375d11842abb36e63aeb91cad Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 29 Oct 2015 16:53:15 +0100
Subject: Avoid an anomaly when destructing an unknown ident. (Fix bug #4395)

It is too bad that OCaml does not warn when catching an exception over a
closure rather than inside it.
---
 tactics/tacinterp.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 6c125ed2d9..355745d970 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -985,10 +985,10 @@ let interp_induction_arg ist gl arg =
       let try_cast_id id' =
         if Tactics.is_quantified_hypothesis id' gl
         then keep,ElimOnIdent (loc,id')
-        else
-          (try keep,ElimOnConstr (fun env sigma -> sigma,(constr_of_id env id',NoBindings))
+        else keep, ElimOnConstr (fun env sigma ->
+          try sigma, (constr_of_id env id', NoBindings)
           with Not_found ->
-            user_err_loc (loc,"",
+            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."))
       in
       try
-- 
cgit v1.2.3