diff --git a/theories/Algebra/Groups/FreeProduct.v b/theories/Algebra/Groups/FreeProduct.v
index 075a650993a..57fd2e28c18 100644
--- a/theories/Algebra/Groups/FreeProduct.v
+++ b/theories/Algebra/Groups/FreeProduct.v
@@ -731,7 +731,7 @@ Definition freeproduct_ind_homotopy {G H K : Group}
 Proof.
   rapply (freeproduct_ind_hprop _ l r).
   intros x y; nrapply grp_homo_op_agree. (* Slow, ~0.2s. *)
-Time Defined. (* Slow, ~0.15s. *)
+Defined. (* Slow, ~0.15s. *)
 
 Definition freeproduct_rec_beta_inl {G H K : Group}
   (f : G $-> K) (g : H $-> K)
diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v
index 8b72344e748..a29752b1b34 100644
--- a/theories/Algebra/Groups/Group.v
+++ b/theories/Algebra/Groups/Group.v
@@ -278,6 +278,7 @@ Defined.
 (** Group homomorphisms preserve inverses. *)
 Definition grp_homo_inv {G H} (f : GroupHomomorphism G H)
   : forall x, f x^ = (f x)^.
+(* This can also be proved using [:= preserves_inverse.] from Classes/theory/groups.v.  That uses [rewrite] and is marked [Qed]. *)
 Proof.
   intro x.
   apply (inverse_unique (f x)).
diff --git a/theories/Homotopy/HSpace/Core.v b/theories/Homotopy/HSpace/Core.v
index a0b08ac277f..6a883d9d0e6 100644
--- a/theories/Homotopy/HSpace/Core.v
+++ b/theories/Homotopy/HSpace/Core.v
@@ -139,7 +139,7 @@ Definition phomotopy_from_homotopy `{Funext} {A B : pType}
   (m : forall (a : A), (point A) = (point A) -> a = a)
   (q :  m pt == idmap) {f g : B ->* A} (K : f == g)
   : f ==* g
-  := (phomotopy_from_path_arrow m q (path_forall _ _ K)).
+  := phomotopy_from_path_arrow m q (path_forall _ _ K).
 
 (** We specialize to H-spaces. *)
 Definition hspace_phomotopy_from_homotopy `{Funext} {A B : pType}
diff --git a/theories/Modalities/Modality.v b/theories/Modalities/Modality.v
index a1abf512b16..902384dfead 100644
--- a/theories/Modalities/Modality.v
+++ b/theories/Modalities/Modality.v
@@ -513,7 +513,7 @@ Section ModalFact.
   : IsConnMap O (factor1 (image f))
     := inclass1 (image f).
 
-  Global Instance inO_map_factor1_image {A B : Type} (f : A -> B)
+  Global Instance inO_map_factor2_image {A B : Type} (f : A -> B)
   : MapIn O (factor2 (image f))
     := inclass2 (image f).
 
diff --git a/theories/Pointed/pTrunc.v b/theories/Pointed/pTrunc.v
index cef040364cb..5005d73c2e5 100644
--- a/theories/Pointed/pTrunc.v
+++ b/theories/Pointed/pTrunc.v
@@ -159,7 +159,7 @@ Defined.
 
 (** ** Truncatedness of [pForall] and [pMap] *)
 
-(** Buchholtz-van Doorn-Rijke, Theorem 4.2:  Let [j >= -1] and [n >= -2].  When [X] is [j]-connected and [Y] is a pointed family of [j+k+1]-truncated types, the type of pointed sections is [n]-truncated.  We formalize it with [j] replaced with a trunc index [m], and so there is a shift compared to the informal statement. This version also allows [n] to be one smaller than BvDR allow. *)
+(** Buchholtz-van Doorn-Rijke, Theorem 4.2:  Let [j >= -1] and [n >= -2].  When [X] is [j]-connected and [Y] is a pointed family of [j+n+1]-truncated types, the type of pointed sections is [n]-truncated.  We formalize it with [j] replaced with a trunc index [m.+1] to enforce [j >= -1]. This version also allows [n] to be one smaller than BvDR allow. *)
 Definition istrunc_pforall `{Univalence} {m n : trunc_index}
   (X : pType@{u}) {iscX : IsConnected m.+1 X}
   (Y : pFam@{u v} X) {istY : forall x, IsTrunc (n +2+ m) (Y x)}
@@ -175,7 +175,7 @@ Definition istrunc_pmap `{Univalence} {m n : trunc_index} (X Y : pType)
   : IsTrunc n (X ->* Y)
   := istrunc_pforall X (pfam_const Y).
 
-(** We can give a different proof of the [n = -1] case (with the conclusion upgraded to contractibility).  This proof works for any reflective subuniverse and avoids univalence.  Is it possible to generalize this to dependent functions while still avoiding univalence and/or keeping [O] a general RSU or modality?  Can [istrunc_pmap] be proven without univalence?  What about [istrunc_pforall]?  If the [n = -2] or [n = -1] cases can be proven without univalence, the rest can be done inductively without univalence. *)
+(** We can give a different proof of the [n = -1] case (with the conclusion upgraded to contractibility).  This proof works with [Tr (m.+1)] replaced with any reflective subuniverse [O] and doesn't require univalence.  Is it possible to generalize this to dependent functions while still avoiding univalence and/or keeping [O] a general RSU or modality?  Can [istrunc_pmap] be proven without univalence?  What about [istrunc_pforall]?  If the [n = -2] or [n = -1] cases can be proven without univalence, the rest can be done inductively without univalence. *)
 Definition contr_pmap_isconnected_inO `{Funext} (O : ReflectiveSubuniverse)
   (X : pType) `{IsConnected O X} (Y : pType) `{In O Y}
   : Contr (X ->* Y).
diff --git a/theories/Spaces/Nat/Binomial.v b/theories/Spaces/Nat/Binomial.v
index 31c4ec727e0..d4abdb25d0f 100644
--- a/theories/Spaces/Nat/Binomial.v
+++ b/theories/Spaces/Nat/Binomial.v
@@ -96,9 +96,8 @@ Proof.
   (* The case when [m = n]. *)
   { rewrite nat_sub_cancel.
     rewrite nat_mul_one_r.
-    rewrite nat_div_cancel.
-    1: nrapply nat_choose_diag.
-    exact _. }
+    rhs rapply nat_div_cancel.
+    nrapply nat_choose_diag. }
   (* The case with [n.+1] and [m.+1] with [m < n] and an induction hypothesis. *)
   intros m H IHn.
   rewrite_refl nat_choose_succ.
diff --git a/theories/Spaces/Nat/Core.v b/theories/Spaces/Nat/Core.v
index a9c0c88cf97..73bc77f2aa7 100644
--- a/theories/Spaces/Nat/Core.v
+++ b/theories/Spaces/Nat/Core.v
@@ -1580,7 +1580,7 @@ Defined.
 (** ** An induction principle for two variables with a constraint. *)
 Definition nat_double_ind_leq@{u} (P : nat -> nat -> Type@{u})
   (Hn0 : forall n, P n 0)
-  (Hnn : forall n, P n n)
+  (Hnn : forall n, P n.+1 n.+1)
   (IH : forall n m, m < n -> (forall m', m' <= n -> P n m') -> P n.+1 m.+1)
   : forall n m, m <= n -> P n m.
 Proof.
diff --git a/theories/Truncations/Connectedness.v b/theories/Truncations/Connectedness.v
index 6c175b36834..d08ce37de89 100644
--- a/theories/Truncations/Connectedness.v
+++ b/theories/Truncations/Connectedness.v
@@ -48,7 +48,7 @@ Proof.
     (* m = S m' *)
   - apply istrunc_S.
     intros e e'. refine (istrunc_isequiv_istrunc _ (path_extension e e')).
-  (* magically infers: paths in extensions = extensions into paths, which by induction is m'-truncated. *)
+    (* Magically infers: paths in extensions = extensions into paths, which by induction is [m']-truncated. *)
 Defined.
 
 (** ** Connectedness of path spaces *)
@@ -91,9 +91,9 @@ Definition conn_point_elim `{Univalence} (n : trunc_index) {A : pType@{u}} `{IsC
            (P : A -> Type@{u}) `{forall a, IsTrunc n (P a)} (p0 : P (point A))
   : forall a, P a.
 Proof.
-  (** This follows from [conn_point_incl] and [conn_map_elim], but we give a direct proof. *)
+  (* This follows from [conn_point_incl] and [conn_map_elim], but we give a direct proof. *)
   intro a.
-  (** Since [A] is [n+1]-connected, [a0 = a] is [n]-connected, which means that [Tr n (a0 = a)] has an element. *)
+  (* Since [A] is [n+1]-connected, [a0 = a] is [n]-connected, which means that [Tr n (a0 = a)] has an element. *)
   pose proof (p := center (Tr n ((point A) = a))).
   strip_truncations.
   exact (p # p0).