Stream: Elpi users & devs

Topic: Duplicate context entry


view this post on Zulip 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

view this post on Zulip Enrico Tassi (Jul 02 2021 at 12:39):

Oh, in 1.10.x you don't need to Context => anymore

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Jul 02 2021 at 12:40):

some doc here: https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi#L260

view this post on Zulip 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: Feb 04 2023 at 02:03 UTC