Use ltac backtrace in "tactic was not fully applied" error

Fix coq#18119

This adds
~~~
In nested Ltac calls to "run_tac (tactic)" and "tac" (bound to fun _ => destruct n as [| n']), last
call failed.
~~~
to the example from that issue.

plugins/ltac/tacinterp.ml

@@ -1411,7 +1411,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"
@@ -1426,6 +1426,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) ++

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.