diff options
| author |  Farzon Lotfi <farzonl@gmail.com> | 2017-11-02 12:14:27 -0400 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2017-11-02 12:14:27 -0400 |
| commit | 0f66537db5df9a7f5ba9a056fd21ff34e83cc8dc (patch) | |
| tree | eeef8e763c32a3068357a46fb42a2dfc04500bf4 /tactics | |
| parent | e5659c8ffe735c530a707a61c692a3af21a79a9a (diff) | |
Update tactics.ml
fix spelling mistake. reword message to be in the Present Perfect tense instead of the 3rd person present because action is completed with respect to the theorem not some unknown third person.
Diffstat (limited to 'tactics')
| -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 -> |