Mercurial > cpdt > repo

diff src/InductiveTypes.v @ 302:7b38729be069

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweak mark-up to support coqdoc 8.3
author Adam Chlipala <adam@chlipala.net>
date Mon, 17 Jan 2011 15:12:30 -0500
parents 2c88fc1dbe33
children d5787b70cf48
line wrap: on
line diff
--- a/src/InductiveTypes.v	Mon Jan 17 11:42:09 2011 -0500
+++ b/src/InductiveTypes.v	Mon Jan 17 15:12:30 2011 -0500
@@ -52,7 +52,8 @@
 (** The goal changes to:
 [[
  tt = tt
-]] *)
+]]
+*)
 
   (** ...which we can discharge trivially. *)
 
@@ -370,7 +371,8 @@
        (forall n : nat_btree,
         P n -> forall (n0 : nat) (n1 : nat_btree), P n1 -> P (NNode n n0 n1)) ->
        forall n : nat_btree, P n
-]] *)
+]]
+*)
 
 
 (** * Parameterized Types *)
@@ -895,7 +897,8 @@
   Notation            Scope     
   "A /\ B" := and A B  : type_scope
                         (default interpretation)
-]] *)
+]]
+*)
 
 Print and.
 (** %\vspace{-.15in}% [[
@@ -1102,7 +1105,8 @@
   ============================
    True
  
-]] *)
+]]
+*)
 
   trivial.
 Qed.