Stream: Coq devs & plugin devs

Topic: Name binding behavior in Ltac


view this post on Zulip 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.)

view this post on Zulip Ali Caglayan (Jan 20 2022 at 21:29):

Is it this: https://coq.inria.fr/refman/proof-engine/ltac.html#local-definitions-let?

view this post on Zulip Pierre-Marie Pédrot (Jan 20 2022 at 21:40):

that's called the strict mode

view this post on Zulip 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)

view this post on Zulip 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: Jun 04 2023 at 19:30 UTC