# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1260566309 18000
# Node ID 76043a960a38b0c226cb0a9504a2478a560a781c
# Parent  0f45421cae2109ab1d2ac4e345d2fc63602f5462
Proofreading pass over Firstorder

diff -r 0f45421cae21 -r 76043a960a38 src/Firstorder.v
--- a/src/Firstorder.v	Fri Dec 11 16:07:27 2009 -0500
+++ b/src/Firstorder.v	Fri Dec 11 16:18:29 2009 -0500
@@ -60,7 +60,7 @@
 
   Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
 
-  (** Now we define the judgment itself, using a [where] clause to associate a notation definition. *)
+  (** Now we define the judgment itself, for variable typing, using a [where] clause to associate a notation definition. *)
 
   Inductive lookup : ctx -> var -> type -> Prop :=
   | First : forall x t G,