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.
idtac is not enough so it's not a thunking issue, I guess.
some sort of focusing issue maybe? what happens if you wrap in
match goal with |- _ => $code end?
Same problem with that. The code is in a
Hint Extern. Does that make a difference?
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