Stream: Ltac2

Topic: Ltac1.of_constr only works after `idtac x`


view this post on Zulip Janno (Sep 16 2022 at 15:01):

I have a bit of Ltac1 code that calls an Ltac2 tactic and passes a constr to it. For some reason, Ltac1.to_constr x returns None. This would be fine (albeit mysterious) if it wasn't for the fact that if I print the value in ltac1 (using idtac x) the problem suddenly disappears and Ltac1.to_constr returns the Some ... Does anyone know why this could happen? There doesn't seem to be a way to print Ltac1.t values in Ltac2 so I don't really know how else to debug this.

view this post on Zulip Janno (Sep 16 2022 at 15:01):

Just idtac is not enough so it's not a thunking issue, I guess.

view this post on Zulip Gaƫtan Gilbert (Sep 16 2022 at 15:07):

some sort of focusing issue maybe? what happens if you wrap in match goal with |- _ => $code end?

view this post on Zulip Janno (Sep 16 2022 at 15:17):

Same problem with that. The code is in a Hint Extern. Does that make a difference?

view this post on Zulip Janno (Sep 16 2022 at 15:48):

Oh, the problem is more interesting: idtac x actually fails so the Ltac2 code never runs. Back to the drawing board, I guess.


Last updated: Jan 31 2023 at 10:01 UTC