Fix typo and more Coqdoc.

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.