diff options
| author | coqbot-app[bot] | 2020-09-12 20:00:32 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-12 20:00:32 +0000 |
| commit | e0696ef1db06dbe32c95ac16b9c54d6b3624dff0 (patch) | |
| tree | b4c98d06350c274b46951470ab48aec11dbf35fa /test-suite/success | |
| parent | 5b62a6908202eef2c40d2f4989d8d21d0f6c3e16 (diff) | |
| parent | ad7140a7127b147caf20d7c3803b918e3c6776f5 (diff) | |
Merge PR #12979: Uniformize names for number literals between parsing and refman
Reviewed-by: herbelin
Reviewed-by: jfehrle
Ack-by: Zimmi48
Ack-by: proux01
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/NumeralNotationsNoLocal.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/NumeralNotationsNoLocal.v b/test-suite/success/NumeralNotationsNoLocal.v index ea3907ef8a..fe97f10ddf 100644 --- a/test-suite/success/NumeralNotationsNoLocal.v +++ b/test-suite/success/NumeralNotationsNoLocal.v @@ -5,7 +5,7 @@ Delimit Scope unit11_scope with unit11. Goal True. evar (to_uint : unit11 -> Decimal.uint). evar (of_uint : Decimal.uint -> unit11). - Fail Numeral Notation unit11 of_uint to_uint : uint11_scope. + Fail Number Notation unit11 of_uint to_uint : uint11_scope. exact I. Unshelve. all: solve [ constructor ]. |