# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1357508062 18000
# Node ID 2d66421b8aa115549cf48a95a732fa07b001fe67
# Parent  5025a401ad9e54aa62f05e8206ed79e0000a2769
Small wording change suggested by a proofreader

diff -r 5025a401ad9e -r 2d66421b8aa1 src/Reflection.v
--- a/src/Reflection.v	Sun Jan 06 16:23:26 2013 -0500
+++ b/src/Reflection.v	Sun Jan 06 16:34:22 2013 -0500
@@ -659,7 +659,7 @@
 (* begin thide *)
 (** The action of the [quote] tactic above may seem like magic.  Somehow it performs equality comparison between subterms of arbitrary types, so that these subterms may be represented with the same reified variable.  While [quote] is implemented in OCaml, we can code the reification process completely in Ltac, as well.  To make our job simpler, we will represent variables as [nat]s, indexing into a simple list of variable values that may be referenced.
 
-   Step one of the process is to crawl over a term, building a duplicate-free list of all values that appear in positions we will encode as variables.  A useful helper function adds an element to a list, maintaining lack of duplicates.  Note how we use Ltac pattern matching to implement an equality test on Gallina terms; this is simple syntactic equality, not even the richer definitional equality.  We also represent lists as nested tuples, to allow different list elements to have different Gallina types. *)
+   Step one of the process is to crawl over a term, building a duplicate-free list of all values that appear in positions we will encode as variables.  A useful helper function adds an element to a list, preventing duplicates.  Note how we use Ltac pattern matching to implement an equality test on Gallina terms; this is simple syntactic equality, not even the richer definitional equality.  We also represent lists as nested tuples, to allow different list elements to have different Gallina types. *)
 
 Ltac inList x xs :=
   match xs with