aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
diff options
context:
space:
mode:
authorSimon Friis Vindum2020-12-03 10:44:06 +0100
committerSimon Friis Vindum2020-12-06 07:41:31 +0100
commita996fb740fa26d899e83a62324f12f62b17c0bc9 (patch)
tree904948200b0412f350d9a935dff6204b75954f56 /test-suite/output
parent2eeeba76598258bd5691a9825fd888c350fbcef3 (diff)
Fix spelling in warning entry
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/bug_12908.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/bug_12908.v b/test-suite/output/bug_12908.v
index 6f7be22fa0..7ab218a27a 100644
--- a/test-suite/output/bug_12908.v
+++ b/test-suite/output/bug_12908.v
@@ -7,7 +7,7 @@ Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n.
End A.
Module B.
-(* Test that an overriden scoped notation is deactivated *)
+(* Test that an overridden scoped notation is deactivated *)
Infix "*" := mult' : nat_scope.
Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n.
End B.