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)
Last updated: Feb 02 2023 at 13:03 UTC