@Pierre-Marie Pédrot : I am rewriting some Ltac code from Princeton VST into Ltac2 and struggle reconstructing the
exploit tactic from CompCert - which is as far as I understand a rigid version of eapply - in Ltac2, so far without success.
The issues I came accross:
refinedoes not seem to accept holes (
eexactis in Ltac1
eexactbasically works but leaves shelved goals, while Ltac1
refineleaves unshelved goals
refineor the complete
exploittactic complains that some of the goals which should be left as open goals cannot be solved
@Michael Soegtrop Maybe you are looking for
Control.refine (fun () => '(term with holes here))?
In Ltac1, I think
eexact maybe uses old unification while
refine definitely uses new unification. Furthermore,
refine is supposed to leave holes as unshelved goals (equivalent to
simple refine ...; shelve_unifiable), while I think
eexact is supposed to shelve all goals (a la
simple refine ...; shelve)?
@Jason Gross : thanks! This has the same effect (for the specific case of 20 arguments) as the Ltac1 tactic:
Ltac2 exploit20 (x : constr) := Control.refine (fun () => '(modusponens _ _ ($x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)); Control.shelve_unifiable ().
So a difference between Ltac2
refine and Ltac
refine is that Ltac1
refine includes a
Do you think I should open an issue to adjust the behaviour of Ltac2
refine (the notation, not the
Control.refine function) to that of Ltac1
Last updated: Nov 29 2023 at 22:01 UTC