Mercurial > cpdt > repo
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 *)