diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 19efe74eb7c8..d3960eb4e4df 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1410,7 +1410,7 @@ and tactic_of_value ist vle = let tac = name_if_glob appl (eval_tactic_ist ist t) in let (stack, _) = trace in Profile_ltac.do_profile stack (catch_error_tac_loc loc stack tac) - | VFun (appl,_,loc,vmap,vars,_) -> + | VFun (appl,(stack,_),loc,vmap,vars,_) -> let tactic_nm = match appl with UnnamedAppl -> "An unnamed user-defined tactic" @@ -1425,6 +1425,7 @@ and tactic_of_value ist vle = List.map (fun (arg,_) -> Names.Id.to_string arg) (Names.Id.Map.bindings vmap) in let numgiven = List.length givenargs in let info = Exninfo.reify () in + catch_error_tac stack @@ Tacticals.tclZEROMSG ~info Pp.(str tactic_nm ++ str " was not fully applied:" ++ spc() ++ str "There is a missing argument for variable" ++ spc() ++ Name.print (List.hd vars) ++ diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out index a7e84d261bb7..71192627c40f 100644 --- a/test-suite/output/ltac_missing_args.out +++ b/test-suite/output/ltac_missing_args.out @@ -1,30 +1,37 @@ File "./output/ltac_missing_args.v", line 11, characters 2-11: The command has indeed failed with message: +Ltac call to "foo" failed. The user-defined tactic "foo" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. File "./output/ltac_missing_args.v", line 12, characters 2-11: The command has indeed failed with message: +Ltac call to "bar" failed. The user-defined tactic "bar" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. File "./output/ltac_missing_args.v", line 13, characters 2-16: The command has indeed failed with message: +Ltac call to "bar" failed. The user-defined tactic "bar" was not fully applied: There is a missing argument for variable y and 1 more, 1 argument was provided. File "./output/ltac_missing_args.v", line 14, characters 2-11: The command has indeed failed with message: +In nested Ltac calls to "baz" and "foo", last call failed. The user-defined tactic "baz" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. File "./output/ltac_missing_args.v", line 15, characters 2-11: The command has indeed failed with message: +In nested Ltac calls to "qux" and "bar", last call failed. The user-defined tactic "qux" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. File "./output/ltac_missing_args.v", line 16, characters 2-36: The command has indeed failed with message: +In nested Ltac calls to "mydo" and "tac" (bound to +fun _ _ => idtac), last call failed. The user-defined tactic "mydo" was not fully applied: There is a missing argument for variable _, no arguments at all were provided. @@ -40,6 +47,7 @@ There is a missing argument for variable _, no arguments at all were provided. File "./output/ltac_missing_args.v", line 19, characters 2-16: The command has indeed failed with message: +In nested Ltac calls to "rec" and "rec", last call failed. The user-defined tactic "rec" was not fully applied: There is a missing argument for variable x, no arguments at all were provided.