aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success')
-rw-r--r--test-suite/success/NumeralNotationsNoLocal.v2
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 ].