Enzo Crance (Jul 02 2021 at 12:34): Enzo Crance (Jul 02 2021 at 12:34):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
Enrico Tassi (Jul 02 2021 at 12:39):Oh, in 1.10.x you don't need to Context => anymore
Enrico Tassi (Jul 02 2021 at 12:39):It's one of the things I want to explain in the tutorials. There are 2 kind of goals, regular and sealed
Enrico Tassi (Jul 02 2021 at 12:40):some doc here: https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi#L260
Enrico Tassi (Jul 02 2021 at 12:45):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: Oct 13 2024 at 01:02 UTC