diff src/Reflection.v @ 302:7b38729be069

Tweak mark-up to support coqdoc 8.3
author Adam Chlipala <adam@chlipala.net>
date Mon, 17 Jan 2011 15:12:30 -0500
parents b441010125d4
children d5787b70cf48
line wrap: on
line diff
--- a/src/Reflection.v	Mon Jan 17 11:42:09 2011 -0500
+++ b/src/Reflection.v	Mon Jan 17 15:12:30 2011 -0500
@@ -593,7 +593,8 @@
               (And Truth (And Truth (And Truth (And Truth Falsehood))))))
         Falsehood))
      : True /\ True /\ True /\ True /\ True /\ True /\ False --> False
-    ]] *)
+    ]]
+    *)
 
 Theorem mt4' : True /\ True /\ True /\ True /\ True /\ True /\ False -> False.
   tauto.
@@ -616,7 +617,8 @@
                and_ind (fun (_ : True) (H11 : False) => False_ind False H11)
                  H9) H7) H5) H3) H1) H
      : True /\ True /\ True /\ True /\ True /\ True /\ False -> False
-    ]] *)
+    ]]
+    *)
 
 
 (** * Exercises *)