Stream: Coq devs & plugin devs

Topic: moving constructor in "new" proof engine and to evarconv


view this post on Zulip Hugo Herbelin (Aug 23 2021 at 10:31):

Hi, I made a quick experiment at moving the constructor tactic to the new proof engine and to evarconv. This is not so easy and I'm blocking at the level of the interaction between typeclass resolution and heuristics. Probably not worth to insist at this stage knowing that that would be subsumed by unifall but I'm curious about the status of this typeclasses/heuristics interaction. What is done, and in which order, when calling a tactics (cc @Maxime Dénès , @Matthieu Sozeau)?

view this post on Zulip Maxime Dénès (Aug 23 2021 at 10:35):

It does ring a bell. I don't recall exactly where we were with constructor, though.

view this post on Zulip Maxime Dénès (Aug 23 2021 at 10:36):

Already when porting clenvs to evarconv, constructor had shown some subtle behavior changes, IIRC.

view this post on Zulip Ali Caglayan (Aug 23 2021 at 12:39):

It would be nice if the user had control over what is considered a constructor. For inductive types, its a no brainer, but for records, sometimes you might want a "smart constructor". If we could somehow label definitions (perhaps with an attribute) we could override what is considered "Build_X" for X. Also finer control, like we have for refine would be nice simple, notypeclasses etc.


Last updated: Oct 21 2021 at 20:02 UTC