Janno (Mar 19 2021 at 19:38): 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?)
Gaëtan Gilbert (Mar 19 2021 at 20:06):
bounded_constr_pat_discr_env
that doesn't exist
Janno (Mar 19 2021 at 20:09):Sorry, the _env suffix was added by my fingers without my brain's input!
Janno (Mar 19 2021 at 20:10):But I think the right code path is actually the one with _st at the end.
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 :(
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: Jun 08 2023 at 04:01 UTC