Stream: Coq devs & plugin devs

Topic: Debugging Btermdn treatment of variables

view this post on Zulip Janno (Mar 19 2021 at 19:38):

I am using Btermdn and I am finally seeing something that I had previously suspected to also affect typeclass search: Using Btermdn's pattern function with the transparency state of a Hint Variables Transparent database , universally quantified variables of both the section and the current lemma are translated to _. If I set Hint Variables Opaque : my_db, the variables appear in the pattern as themselves. I absolutely do not understand how this happens. From my reading of bounded_constr_pat_discr_st it seems like Environ.evaluable_named would have to return true for a LocalAssum, which it simply doesn't.
I already wondered if maybe I am using the wrong environment but even Proofview.tclENV should give correct readings for section variables and they are affected just like local variables. Does anyone have any clues as to what might be going on here or how I could debug it further? (Or is this behavior intentional?)

view this post on Zulip Gaƫtan Gilbert (Mar 19 2021 at 20:06):


that doesn't exist

view this post on Zulip Janno (Mar 19 2021 at 20:09):

Sorry, the _env suffix was added by my fingers without my brain's input!

view this post on Zulip Janno (Mar 19 2021 at 20:10):

But I think the right code path is actually the one with _st at the end.

view this post on Zulip Janno (Mar 19 2021 at 20:11):

I have been staring at this code for quite a while and it's just alphabet soup to me now :(

view this post on Zulip Janno (Mar 22 2021 at 16:40):

I am still puzzled by this behavior. I can't share my code but if it helps I can share some debug output / generally explain what my code is doing.

Last updated: Oct 16 2021 at 03:02 UTC