aboutsummaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Classes/Init.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 8a04206bb2..8732305953 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -23,7 +23,7 @@ Typeclasses Opaque id const flip compose arrow impl iff not all.
(** Apply using the same opacity information as typeclass proof search. *)
-Ltac class_apply c := autoapply c using typeclass_instances.
+Ltac class_apply c := autoapply c with typeclass_instances.
(** The unconvertible typeclass, to test that two objects of the same type are
actually different. *)