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.
I think it has section variables though
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.
don't see how any of those would matter
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.
If you ask why it's a state and not a reader, it can change due to calls to
abstract and the like.
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
Last updated: Oct 16 2021 at 02:03 UTC