Stream: Ltac2

Topic: ✔ `constr:(...)` printing


view this post on Zulip Jason Gross (Oct 23 2022 at 08:30):

When does Ltac2 decide to print constrs as ...? (Context: https://github.com/coq/coq/issues/16716)

view this post on Zulip Gaëtan Gilbert (Oct 23 2022 at 09:26):

answer in issue

view this post on Zulip Jason Gross (Oct 23 2022 at 09:52):

Thanks!

view this post on Zulip Notification Bot (Oct 23 2022 at 09:52):

Jason Gross has marked this topic as resolved.


Last updated: Apr 14 2024 at 09:39 UTC