diff options
| author | Guillaume Melquiond | 2015-10-29 16:53:15 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-10-29 16:54:01 +0100 |
| commit | dc13be3390c7b1d375d11842abb36e63aeb91cad (patch) | |
| tree | 37e627a81ebe55b97e78525e70b1e251da801324 | |
| parent | 654b69cbeb55a0cab3c2328d73355ad2510d1a85 (diff) | |
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.
| -rw-r--r-- | tactics/tacinterp.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 |