diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-11-18 15:58:17 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-11-18 15:59:04 +0100 |
| commit | 6f88442be8275361a7b68fd56d40976fdee9f4d5 (patch) | |
| tree | 83eb1fd96609442895ecb021152cd996a746b4d1 /tactics/tacinterp.ml | |
| parent | 23e6963a8168756f225ea2ae75fcf2af6952c6c3 (diff) | |
Improve error message.
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 355745d97..d24412942 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 *) |