Mercurial > cpdt > repo
diff src/Predicates.v @ 205:f05514cc6c0d
'make doc' works with 8.2
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 06 Nov 2009 12:15:05 -0500 |
parents | 71ade09024ac |
children | 90af611e2993 |
line wrap: on
line diff
--- a/src/Predicates.v Fri Nov 06 10:52:43 2009 -0500 +++ b/src/Predicates.v Fri Nov 06 12:15:05 2009 -0500 @@ -73,6 +73,7 @@ (** [[ Inductive False : Prop := + ]] *) (** We can conclude anything from [False], doing case analysis on a proof of [False] in the same way we might do case analysis on, say, a natural number. Since there are no cases to consider, any such case analysis succeeds immediately in proving the goal. *)