aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success')
-rw-r--r--test-suite/success/Typeclasses.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 563651cfa5..7acaa92b89 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -190,7 +190,7 @@ Record Monad {m : Type -> Type} := {
Print Visibility.
Print unit.
-Arguments unit {m m0 α}.
+Arguments unit {m _ α}.
Arguments Monad : clear implicits.
Notation "'return' t" := (unit t).