Skip to content

Commit

Permalink
Use ltac backtrace in "tactic was not fully applied" error
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
SkySkimmer committed Oct 3, 2023
1 parent 227a087 commit 311de26
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion plugins/ltac/tacinterp.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand All @@ -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) ++
Expand Down

0 comments on commit 311de26

Please sign in to comment.