--- a/src/Large.v	Sun Feb 02 10:51:18 2020 -0500
+++ b/src/Large.v	Sun Jul 31 14:48:22 2022 -0400
@@ -258,9 +258,9 @@
    eval e1 * eval e3 * eval e4 = eval e1 * eval e2
    ]]
 
-   The [crush] tactic does not know how to finish this goal.  We could finish the proof manually. *)
+   The [crush] tactic does not know how to finish this goal.  We could finish the proof manually.  Just kidding, the standard library got smarter, and the following is now redundant! *)
 
-  rewrite <- IHe2; crush.
+  (*rewrite <- IHe2; crush.*)
 
   (** However, the proof would be easier to understand and maintain if we separated this insight into a separate lemma. *)
 
@@ -460,7 +460,8 @@
   (** What is [t] doing to get us to this point?  The %\index{tactics!info}%[info] command can help us answer this kind of question.  (As of this writing, [info] is no longer functioning in the most recent Coq release, but I hope it returns.) *)
 
   Undo.
-  info t.
+  (*info*) t.
+  (* Too bad: recent Coq versions removed [info]. *)
 
   (* begin hide *)
   (* begin thide *)
@@ -515,7 +516,7 @@
 
   Undo.
 
-  info autorewrite with core in *.
+  (*info*) autorewrite with core in *.
   (** %\vspace{-.15in}%[[
  == refine (eq_ind_r (fun n : nat => n = eval e1 * eval e2) _
               (confounder (reassoc e1) e3 e4)).
@@ -566,7 +567,7 @@
 
 (* begin thide *)
     Restart.
-    info eauto 6.
+    (*info*) eauto 6.
     (** %\vspace{-.15in}%[[
  == intro x; intro y; intro H; intro H0; intro H4;
        simple eapply trans_eq.