Skip to content

ltac1 bridge is sensitive to name? #912

@patrick-nicodemus

Description

@patrick-nicodemus

Not sure if this is specific to call-ltac1 or elsewhere.

Ltac revwrap x := revert x.

Elpi Tactic rev_ltac.
Elpi Accumulate lp:{{ 

  solve (goal [def Eigen Name Typ Body|L] Raw Ty Evar Args) GL :-
    coq.ltac.call-ltac1 "revwrap"
      (goal [def Eigen Name Typ Body|L] Raw Ty Evar [trm Eigen])
      GL.

  solve (goal [decl Eigen Name Typ|L] Raw Ty Evar Args) GL :-
    coq.ltac.call-ltac1 "revwrap"
      (goal [decl Eigen Name Typ|L] Raw Ty Evar [trm Eigen])
      GL.
}}.

this code works as desired but if I change it from coq.ltac.call-ltac1 "revwrap" (goal def Eigen Name ... to coq.ltac.call-ltac1 "revwrap" (goal def Eigen Name2 ... it breaks. So goals are sensitive to the value of Name, at least across the ltac1 bridge?

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions