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: Oct 12 2024 at 11:01 UTC