changeset 485:2d66421b8aa1

Small wording change suggested by a proofreader
author Adam Chlipala <adam@chlipala.net>
date Sun, 06 Jan 2013 16:34:22 -0500
parents 5025a401ad9e
children f2286f6512f8
files src/Reflection.v
diffstat 1 files changed, 1 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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