Stream: Coq devs & plugin devs

Topic: globalize0 behaviour

view this post on Zulip František Farka (May 30 2023 at 10:41):

I am toying with extending Reset Initial with optional module to replace topfile passed to coqtop from the command line.
The code is here:

When I use globalize0 to update topfile in process_back_meta_command (stm/, l. 2589 here), the value is set only temporarily and there is the old value on the next command.

I cannot figure out where is the set value rolled back and by what code.

There is a test case, the commands I use to run it are in the PR.

Can anyone point me to why this is happening?

Last updated: Dec 05 2023 at 12:01 UTC