From 0f66537db5df9a7f5ba9a056fd21ff34e83cc8dc Mon Sep 17 00:00:00 2001 From: Farzon Lotfi Date: Thu, 2 Nov 2017 12:14:27 -0400 Subject: 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. --- tactics/tactics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -> -- cgit v1.2.3