diff --git a/theories/base.v b/theories/base.v
index b76f16a28083e3f570ddf870af8cba9e33fa557b..da1cc243d1845d1483aa3f1487e6d08ed6acd099 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -11,8 +11,8 @@ From Coq.Program Require Export Basics Syntax.
 
 (** * Enable implicit generalization. *)
 (** This option enables implicit generalization in arguments of the form
-   `{...} (i.e., anonymous arguments).  Unfortunately, it also enables
-   implicit generalization in `Instance`.  We think that the fact taht both
+   [`{...}] (i.e., anonymous arguments).  Unfortunately, it also enables
+   implicit generalization in [Instance].  We think that the fact that both
    behaviors are coupled together is a [bug in
    Coq](https://github.com/coq/coq/issues/6030). *)
 Global Generalizable All Variables.