Mercurial > cpdt > repo
diff src/Large.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 | 4662b6f099b0 |
children | d5787b70cf48 |
line wrap: on
line diff
--- a/src/Large.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/Large.v Mon Jan 17 15:12:30 2011 -0500 @@ -123,7 +123,8 @@ Error: The reference IHe1 was not found in the current environment. - ]] *) + ]] + *) Abort. @@ -184,7 +185,8 @@ Error: Expects a disjunctive pattern with 3 branches. - ]] *) + ]] + *) Abort. @@ -540,7 +542,8 @@ Time eauto 6. (** [[ Finished transaction in 0. secs (0.068004u,0.s) -]] *) +]] +*) Qed. @@ -722,7 +725,8 @@ (** %\vspace{-.15in}% [[ IntTheorems.unique_ident : forall e' : Int.G, (forall a : Int.G, Int.f e' a = a) -> e' = Int.e - ]] *) + ]] + *) Theorem unique_ident : forall e', (forall a, e' + a = a) -> e' = 0. exact IntTheorems.unique_ident.