Mercurial > cpdt > repo

diff src/Generic.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 b027b39606ed
children b1fead9f68f2
line wrap: on
line diff
--- a/src/Generic.v	Fri Jul 27 15:41:06 2012 -0400
+++ b/src/Generic.v	Fri Jul 27 16:47:28 2012 -0400
@@ -361,7 +361,9 @@
      *)
 
 (* begin hide *)
+(* begin thide *)
 Definition append' := append.
+(* end thide *)
 (* end hide *)
 
 (** Some of these simplified terms seem overly complex because we have turned off simplification of calls to [append], which is what uses of the [++] operator desugar to.  Selective [++] simplification would combine adjacent string literals, yielding more or less the code we would write manually to implement this printing scheme. *)
@@ -647,7 +649,9 @@
   induction r; crush.
 
   (* begin hide *)
+  (* begin thide *)
   Definition pred' := pred.
+  (* end thide *)
   (* end hide *)
 
   (** The base case is discharged automatically, and the inductive case looks like this, where [H] is the outer IH (for induction over [T] values) and [IHn] is the inner IH (for induction over the recursive arguments).