Janno (Sep 16 2022 at 15:01): 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.
Janno (Sep 16 2022 at 15:01):Just idtac is not enough so it's not a thunking issue, I guess.
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?
Janno (Sep 16 2022 at 15:17):Same problem with that. The code is in a Hint Extern. Does that make a difference?
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: Oct 12 2024 at 13:01 UTC