From 028db341f3cb924c2d1b3a9e0fa5666425130f90 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Thu, 9 Feb 2017 11:15:51 -0500 Subject: Report missing tactic arguments in error message Augments "A fully applied tactic is expected" with the list of missing arguments to the tactic. Addresses [bug 5344](https://coq.inria.fr/bugs/show_bug.cgi?id=5344). --- plugins/ltac/tacinterp.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'plugins/ltac/tacinterp.ml') diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index aa646aa51..54bec3967 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1422,7 +1422,14 @@ and tactic_of_value ist vle = extra = TacStore.set ist.extra f_trace []; } in let tac = name_if_glob appl (eval_tactic ist t) in Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac) - | (VFun _|VRec _) -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.") + | VFun (_, _, _,vars,_) -> + let numargs = List.length vars in + Tacticals.New.tclZEROMSG + (str "A fully applied tactic is expected:" ++ spc() ++ Pp.str "missing " ++ + Pp.str (String.plural numargs "argument") ++ Pp.str " for " ++ + Pp.str (String.plural numargs "variable") ++ Pp.str " " ++ + pr_enum pr_name vars ++ Pp.str ".") + | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.") else if has_type vle (topwit wit_tactic) then let tac = out_gen (topwit wit_tactic) vle in tactic_of_value ist tac -- cgit v1.2.3