### changeset 271:aa3c054afce0

Some bug fixes while working on JFR version
author Adam Chlipala Mon, 19 Apr 2010 16:49:26 -0400 fd46d077b952 19fbda8a8117 src/Equality.v src/Subset.v 2 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/Equality.v	Wed Feb 03 08:17:02 2010 -0500
+++ b/src/Equality.v	Mon Apr 19 16:49:26 2010 -0400
@@ -574,7 +574,7 @@

(** There is no quick way to write such a proof by tactics, but the underlying proof term that we want is trivial.

-   Suppose that we want to use [UIP_refl'] to establish another lemma of the kind of we have run into several times so far. *)
+   Suppose that we want to use [UIP_refl'] to establish another lemma of the kind we have run into several times so far. *)

Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x),
O = match pf with refl_equal => O end.
--- a/src/Subset.v	Wed Feb 03 08:17:02 2010 -0500
+++ b/src/Subset.v	Mon Apr 19 16:49:26 2010 -0400
@@ -71,7 +71,7 @@

(** We expand the type of [pred] to include a %\textit{%#<i>#proof#</i>#%}% that its argument [n] is greater than 0.  When [n] is 0, we use the proof to derive a contradiction, which we can use to build a value of any type via a vacuous pattern match.  When [n] is a successor, we have no need for the proof and just return the answer.  The proof argument can be said to have a %\textit{%#<i>#dependent#</i>#%}% type, because its type depends on the %\textit{%#<i>#value#</i>#%}% of the argument [n].

-One aspects in particular of the definition of [pred_strong1] that may be surprising.  We took advantage of [Definition]'s syntactic sugar for defining function arguments in the case of [n], but we bound the proofs later with explicit [fun] expressions.  Let us see what happens if we write this function in the way that at first seems most natural.
+One aspect in particular of the definition of [pred_strong1] may be surprising.  We took advantage of [Definition]'s syntactic sugar for defining function arguments in the case of [n], but we bound the proofs later with explicit [fun] expressions.  Let us see what happens if we write this function in the way that at first seems most natural.

[[
Definition pred_strong1' (n : nat) (pf : n > 0) : nat :=