Merge PR coq#18120: Use ltac backtrace in "tactic was not fully appli…

…ed" error Reviewed-by: herbelin Co-authored-by: herbelin <[email protected]>
Villetaneuse · Oct 5, 2023 · 72277c3 · 72277c3
2 parents d5b30cb + 53400b8
commit 72277c3
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 1 deletion.
diff --git 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
@@ -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.