Mercurial > cpdt > repo
changeset 323:3513d8b0531a
thide parsing-motivating definitions at start of Predicates
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Tue, 20 Sep 2011 11:08:05 -0400 |
| parents | 98e0d957df16 |
| children | 06d11a6363cd |
| files | src/Predicates.v |
| diffstat | 1 files changed, 2 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Predicates.v Mon Sep 19 14:04:09 2011 -0400 +++ b/src/Predicates.v Tue Sep 20 11:08:05 2011 -0400 @@ -16,6 +16,7 @@ (* Extra definitions to get coqdoc to choose the right fonts. *) +(* begin thide *) Inductive unit := tt. Inductive Empty_set := . Inductive bool := true | false. @@ -26,6 +27,7 @@ Inductive ex := ex_intro. Inductive eq := refl_equal. Reset unit. +(* end thide *) (* end hide *) (** %\chapter{Inductive Predicates}% *)