# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1343316166 14400
# Node ID b027b39606ed4e2757c5877e1bf1ef25245372d1
# Parent  5e6b76ca14dee4232cff76a897b0ad8a92a82c2c
Pass through Generic, to incorporate new coqdoc features

diff -r 5e6b76ca14de -r b027b39606ed src/Generic.v
--- a/src/Generic.v	Thu Jul 26 11:09:48 2012 -0400
+++ b/src/Generic.v	Thu Jul 26 11:22:46 2012 -0400
@@ -360,6 +360,10 @@
      ]]
      *)
 
+(* begin hide *)
+Definition append' := append.
+(* 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. *)
 
 
@@ -642,6 +646,10 @@
 
   induction r; crush.
 
+  (* begin hide *)
+  Definition pred' := pred.
+  (* 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).
      [[
   H : forall i : fin (S n),