Stream: Elpi users & devs

Topic: refine failure when everything typechecks

Enzo Crance (Jul 06 2023 at 15:13):

I am struggling with closing some proofs in Elpi.

Everything goes through elaborate-skeleton and typecheck when in Elpi with ok results, the proof I am trying to apply is accepted by Coq if I copy-paste it in an exact call in Ltac
BUT :

• a call to refine.typecheck makes the tactic fail;
• a call to refine makes the tactic output not a goal seal.

The last call outputs my proof in Elpi format as well as some suspended evar goals that I don't understand. Could the problem come from there? Is it possible to clear these evar goals?

Enrico Tassi (Jul 06 2023 at 18:31):

Give me a way to reproduce and I'll check it tomorrow morning

Last updated: Oct 13 2024 at 01:02 UTC