--- a/src/Reflection.v	Sun Apr 21 16:09:55 2019 -0400
+++ b/src/Reflection.v	Sun Feb 02 10:46:14 2020 -0500
@@ -386,9 +386,9 @@
 
 (** Now we are ready to revisit our earlier tautology solver example.  We want to broaden the scope of the tactic to include formulas whose truth is not syntactically apparent.  We will want to allow injection of arbitrary formulas, like we allowed arbitrary monoid expressions in the last example.  Since we are working in a richer theory, it is important to be able to use equalities between different injected formulas.  For instance, we cannot prove [P -> P] by translating the formula into a value like [Imp (Var P) (Var P)], because a Gallina function has no way of comparing the two [P]s for equality.
 
-   To arrive at a nice implementation satisfying these criteria, we introduce the %\index{tactics!quote}%[quote] tactic and its associated library. *)
+   To arrive at a nice implementation satisfying these criteria, we introduce the %\index{tactics!quote}%[quote] tactic and its associated library.  (Actually, this tactic has apparently gone away in the most recent Coq versions, so this section is of historic interest only.) *)
 
-Require Import Quote.
+(*Require Import Quote.
 
 (* begin thide *)
 Inductive formula : Set :=
@@ -654,6 +654,7 @@
     ]]
 
 The traditional [tauto] tactic introduces a quadratic blow-up in the size of the proof term, whereas proofs produced by [my_tauto] always have linear size. *)
+*)
 
 (** ** Manual Reification of Terms with Variables *)