diff options
| author | Tej Chajed | 2017-02-09 11:15:51 -0500 |
|---|---|---|
| committer | Tej Chajed | 2017-03-14 15:55:00 -0400 |
| commit | 028db341f3cb924c2d1b3a9e0fa5666425130f90 (patch) | |
| tree | 74318bee1763040766c94cecab4848b1b2f84e83 | |
| parent | b54892932959a3b16e31f780f7f1b638062b0a95 (diff) | |
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).
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 9 | ||||
| -rw-r--r-- | test-suite/output/ltac_missing_args.out | 21 | ||||
| -rw-r--r-- | test-suite/output/ltac_missing_args.v | 19 |
3 files changed, 48 insertions, 1 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index aa646aa517..54bec39670 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 diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out new file mode 100644 index 0000000000..ae3fd7acc7 --- /dev/null +++ b/test-suite/output/ltac_missing_args.out @@ -0,0 +1,21 @@ +The command has indeed failed with message: +Error: A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +Error: A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +Error: A fully applied tactic is expected: +missing arguments for variables y and _. +The command has indeed failed with message: +Error: A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +Error: A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +Error: A fully applied tactic is expected: missing argument for variable _. +The command has indeed failed with message: +Error: A fully applied tactic is expected: missing argument for variable _. +The command has indeed failed with message: +Error: A fully applied tactic is expected: missing argument for variable _. +The command has indeed failed with message: +Error: A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +Error: A fully applied tactic is expected: missing argument for variable x. diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v new file mode 100644 index 0000000000..8ecd97aa56 --- /dev/null +++ b/test-suite/output/ltac_missing_args.v @@ -0,0 +1,19 @@ +Ltac foo x := idtac x. +Ltac bar x := fun y _ => idtac x y. +Ltac baz := foo. +Ltac qux := bar. +Ltac mydo tac := tac (). +Ltac rec x := rec. + +Goal True. + Fail foo. + Fail bar. + Fail bar True. + Fail baz. + Fail qux. + Fail mydo ltac:(fun _ _ => idtac). + Fail let tac := (fun _ => idtac) in tac. + Fail (fun _ => idtac). + Fail rec True. + Fail let rec tac x := tac in tac True. +Abort.
\ No newline at end of file |