Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

coq.ltac.call "apply" -> "Ltac1 tactic apply not found" #744

Closed
patrick-nicodemus opened this issue Jan 19, 2025 · 1 comment · Fixed by #745
Closed

coq.ltac.call "apply" -> "Ltac1 tactic apply not found" #744

patrick-nicodemus opened this issue Jan 19, 2025 · 1 comment · Fixed by #745

Comments

@patrick-nicodemus
Copy link
Contributor

patrick-nicodemus commented Jan 19, 2025

I am not experienced with Elpi so I might be misunderstanding this. But

Elpi Tactic abc. 
Elpi Accumulate lp:{{
 solve G GL :- coq.ltac.call "apply" [trm {{conj}}] G GL.
}}.

Goal forall(A  B : Prop), A /\ B.
Proof.
    intros A B.
    elpi abc.

This fails for me and prints an error of "Ltac1 tactic apply not found."
Do I need to import something special? I have imported the Prelude and the Ltac module.
rapply works.

@gares
Copy link
Contributor

gares commented Jan 19, 2025

I should document this better: you can only call tactics defined with Ltac. Try calling myapply and add Ltac myapply x := apply x.

@gares gares linked a pull request Jan 19, 2025 that will close this issue
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants