Hi it's me again. Now I got
Duplicate context entry for c0
making the tactic fail right at the beginning. Wasn't happening before the update to 1.11.0 so idk.
solve InitialGoal NewGoals :- InitialGoal = goal Context _ InitialGoalTy _ [trm ETarget, trm LTarget], !, Context => std.do! [ coq.elaborate-skeleton InitialGoalTy _ GroundGoalTy ok,
The last line is what makes it fail. I tried calling this by hand in an
Elpi Query and it works. Weird.
The goal I was trying the tactic on last time was closed and the context was empty. Now I am trying with a
forall T : Type at the beginning, and calling the tactic after
intro T. If that can help
Oh, in 1.10.x you don't need to
Context => anymore
It's one of the things I want to explain in the tutorials. There are 2 kind of goals, regular and sealed
some doc here: https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi#L260
solve applies to a goal which has been
open (https://github.com/LPCIC/coq-elpi/blob/master/elpi/elpi-ltac.elpi#L73) which loads the context for you. If you implement
msolve instead, then it is up to you to open the goal and load the context. It is a change of behavior, sorry for that, but I believe it's better to have the context loaded automatically.
Last updated: Feb 04 2023 at 02:03 UTC