Janno (Aug 19 2021 at 18:40): Janno (Aug 19 2021 at 18:40):I just fixed a bug in a custom OCaml tactic that used Constr_matching functions. I had naively used tclENV to get an environment to feed to is_matching and that worked fine when primitive projections were disabled. However, the parameter of the projection relies on a section variable and with primitive projections enabled retyping failed with <record value> depends on the variable <section variable> which is not declared in the context . The bug is fixed by using Goal.enter_one and then Goal.env. But now I wonder: if tclENV doesn't even contain section variables, what is it good for? Should I ever use it for anything? The docs say it returns the "global" environment of the proof but I don't know what that means.
Gaëtan Gilbert (Aug 19 2021 at 19:04):I think it has section variables though
Janno (Aug 19 2021 at 19:12):I've been doing some more debugging and the result depends on how exactly the tactic is called. I can only reproduce the problem when using something like all: tactic. or ; [tactic|..]. Not when I call the tactic on its own on a single goal. There might be extra complications because the OCaml code is called from an Ltac2 tactic that already uses Control.enter to focus on a single goal.
Gaëtan Gilbert (Aug 19 2021 at 19:31):don't see how any of those would matter
Pierre-Marie Pédrot (Aug 20 2021 at 16:21):The invariants is that tclENV is the "prefix" of the environment needed, and local goal environments are just this env where the named context can be replace.
Pierre-Marie Pédrot (Aug 20 2021 at 16:22):If you ask why it's a state and not a reader, it can change due to calls to abstract and the like.
Pierre-Marie Pédrot (Aug 20 2021 at 16:23):As a end user you shouldn't have to use tclENV I believe (but it's still needed for the internals of the proof engine, since you don't want to call the imperative Global.env function)
Last updated: Jun 04 2023 at 19:30 UTC