What's the name of the thing that controls the fact that let foo _ := pose 0 as m in foo (); pose m.
works at top-level but not in an Ltac script? (And is there an option for it?) (I'm not sure what to search in the refman to quickly find documentation about this.)
Is it this: https://coq.inria.fr/refman/proof-engine/ltac.html#local-definitions-let?
that's called the strict mode
I don't think it's documented in Ltac1 but IIRC it is in Ltac2 (and there is a flag to tweak it)
https://coq.inria.fr/refman/proof-engine/ltac2.html#strict-vs-non-strict-mode
Last updated: Dec 07 2023 at 09:01 UTC