Mercurial > cpdt > repo

diff src/Reflection.v @ 437:8077352044b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A pass over all formatting, after big pile of coqdoc changes
author Adam Chlipala <adam@chlipala.net>
date Fri, 27 Jul 2012 16:47:28 -0400
parents 17d01e51256c
children 0650420c127b
line wrap: on
line diff
--- a/src/Reflection.v	Fri Jul 27 15:41:06 2012 -0400
+++ b/src/Reflection.v	Fri Jul 27 16:47:28 2012 -0400
@@ -58,7 +58,9 @@
     For this example, we begin by using a type from the [MoreSpecif] module (included in the book source) to write a certified evenness checker. *)
 
 (* begin hide *)
+(* begin thide *)
 Definition paartial := partial.
+(* end thide *)
 (* end hide *)
 
 Print partial.
@@ -161,7 +163,9 @@
 Qed.
 
 (* begin hide *)
+(* begin thide *)
 Definition tg := (and_ind, or_introl).
+(* end thide *)
 (* end hide *)
 
 Print true_galore.
@@ -560,7 +564,9 @@
 Qed.
 
 (* begin hide *)
+(* begin thide *)
 Definition nvm := (Node_vm, Empty_vm, End_idx, Left_idx, Right_idx).
+(* end thide *)
 (* end hide *)
 
 Print mt2.
@@ -624,7 +630,9 @@
 Qed.
 
 (* begin hide *)
+(* begin thide *)
 Definition fi := False_ind.
+(* end thide *)
 (* end hide *)
 
 Print mt4'.