Jason Gross (Jan 20 2022 at 21:03): Jason Gross (Jan 20 2022 at 21:03):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.)
Ali Caglayan (Jan 20 2022 at 21:29):Is it this: https://coq.inria.fr/refman/proof-engine/ltac.html#local-definitions-let?
Pierre-Marie Pédrot (Jan 20 2022 at 21:40):that's called the strict mode
Pierre-Marie Pédrot (Jan 20 2022 at 21:41):I don't think it's documented in Ltac1 but IIRC it is in Ltac2 (and there is a flag to tweak it)
Pierre-Marie Pédrot (Jan 20 2022 at 21:41):https://coq.inria.fr/refman/proof-engine/ltac2.html#strict-vs-non-strict-mode
Last updated: Dec 07 2023 at 09:01 UTC