New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Don't make too many coercions reversible by default #18705
Conversation
Cc @ggonthier who noticed the issue |
9d6c5c6
to
429a53a
Compare
🔴 CI failure at commit 429a53a without any failure in the test-suite ✔️ Corresponding job for the base commit 954e315 succeeded ❔ Ask me to try to extract a minimal test case that can be added to the test-suite 🏃
|
Adapt to coq/coq#18705 This is backward compatible (down to Coq 8.16). Co-authored-by: Niels van der Weide <nnmvdw@gmail.com>
The doc reads > By default coercions are not reversible > except for Record fields specified using :>. The previous code was making way too many coercion reversible by default. The new behavior should be closer from the spec in the doc.
429a53a
to
25e9d2a
Compare
@coq/vernac-maintainers this is ready, CI green |
@@ -32,7 +32,7 @@ let declare_variable is_coe ~kind typ univs imps impl name = | |||
let () = | |||
if is_coe = Vernacexpr.AddCoercion then | |||
ComCoercion.try_add_new_coercion | |||
r ~local:true ~reversible:true in | |||
r ~local:true ~reversible:false in |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should reversible
be optional (defaulting to false)?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Probably yes. I guess, my initial intent in not making optional was to avoid forgetting a callsite. But I managed to screw up anyway, so that was probably a bad choice.
The previous code was making way too many coercion reversible by default. | ||
The new behavior should be closer from the spec in the doc |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is less formal language than usual but I don't mind.
@coqbot merge now |
The doc reads
The previous code was making some other coercions (particularly
Coercion foo := bar.
but notCoercion foo : bar >-> baz.
) reversible by default. The new behavior should be closer from the spec in the doc.Added / updated documentation.Documented any new / changed user messages.Updated documented syntax by runningmake doc_gram_rsts
.Overlay (to be merged before the current PR)