diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-03 11:01:16 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-03 11:01:16 +0100 |
| commit | f281a8a88e8fc7c41cc5680db2443d9da33b47b7 (patch) | |
| tree | 2c75844e980840d2d4f25b8a27de936ae3c370f8 | |
| parent | 96a8d73edaa4eba500c440e5d6869fae1af91a12 (diff) | |
| parent | 0f66537db5df9a7f5ba9a056fd21ff34e83cc8dc (diff) | |
Merge PR #6060: Improve error message and fix #6055 (spelling mistake).
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6ab643239..f8f9e029b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1743,7 +1743,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind : let try_apply thm_ty nprod = try let n = nb_prod_modulo_zeta sigma thm_ty - nprod in - if n<0 then error "Applied theorem has not enough premisses."; + if n<0 then error "Applied theorem does not have enough premises."; let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in Clenvtac.res_pf clause ~with_evars ~flags with exn when catchable_exception exn -> |