[Numeral notations] Use Coqlib registered constants #8720
Conversation
7b187f1 to
ff1786e
Compare
| @@ -40,7 +40,7 @@ Notation zero := (D0 Nil). | |||
|
|
|||
| (** For signed integers, we use two constructors [Pos] and [Neg]. *) | |||
|
|
|||
| Inductive int := Pos (d:uint) | Neg (d:uint). | |||
| Variant int := Pos (d:uint) | Neg (d:uint). | |||
There was a problem hiding this comment.
I agree it’s unrelated. But since I was already touching this file, I took the opportunity to tidy it a bit…
plugins/syntax/numeral.ml
Outdated
| CErrors.user_err | ||
| (pr_qualid f ++ str " should go from Decimal.int to " ++ | ||
| pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++ | ||
| fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ | ||
| (if loadZ then str " (require BinNums first)." else str ".")) | ||
| fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used.") |
There was a problem hiding this comment.
What is the reason for dropping the parenthetical? You could instead augment it to say require BinNums or Register a constant as ... first.
Either way, please also update the documentation to match the updated error message.
ff1786e to
cd16bfd
Compare
|
I’ve just updated the error messages and the corresponding documentation. |
| CErrors.user_err | ||
| (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ | ||
| str " to Decimal.int or (option Decimal.int)." ++ fnl () ++ | ||
| str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ | ||
| (if loadZ then str " (require BinNums first)." else str ".")) | ||
| str "Instead of Decimal.int, the types Decimal.uint or Z could be used (you may need to require BinNums or Decimal first).") |
There was a problem hiding this comment.
I think you should only display the part about Require if the types don't resolve / aren't registered. But I don't object strongly.
0efce69 to
c10e3cd
Compare
|
This PR breaks HoTT; the overlay is ready but would break the compatibility of HoTT with Coq 8.9. Thus we wait: 1. that Coq 8.9 is released (or at least the β); 2. that a version of HoTT compatible with said version of Coq is officially tagged; 3. that HoTT merges the overlay. No need to hurry. |
What's the dependency? |
|
I think the answer is in my previous message: #8720 (comment) |
|
I've only seen that tag used for other Coq PRs before but I guess nothing else fits better. |
c10e3cd to
c9eddfe
Compare
c9eddfe to
0fdc539
Compare
|
HoTT has been updated, so this PR is ready now. |
|
Taking this as part of @coq/parsing-maintainers |
Reviewed-by: JasonGross Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: vbgl
Fixes #8564.
Waiting for HoTT release, see #8720 (comment)