Mercurial > cpdt > repo
diff src/Equality.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 | 123f466faedc |
| children | d5787b70cf48 |
line wrap: on
line diff
--- a/src/Equality.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/Equality.v Mon Jan 17 15:12:30 2011 -0500 @@ -87,7 +87,8 @@ ============================ 0 = 0 - ]] *) + ]] + *) reflexivity. Qed. @@ -217,7 +218,8 @@ [[ reflexivity. - ]] *) + ]] + *) Qed. (* end thide *) @@ -268,7 +270,8 @@ User error: Cannot solve a second-order unification problem - ]] *) + ]] + *) Abort. (** Nonetheless, we can adapt the last manual proof to handle this theorem. *) @@ -291,7 +294,8 @@ simple destruct pf. User error: Cannot solve a second-order unification problem - ]] *) + ]] + *) Abort. @@ -429,7 +433,8 @@ fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 = fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 - ]] *) + ]] + *) reflexivity. @@ -716,7 +721,8 @@ ============================ x = y - ]] *) + ]] + *) destruct H. (** [[ @@ -727,7 +733,8 @@ ============================ x = y - ]] *) + ]] + *) rewrite H. (** [[ @@ -737,7 +744,8 @@ | refl_equal => y end = y - ]] *) + ]] + *) rewrite (UIP_refl _ _ x0); reflexivity. Qed. @@ -801,7 +809,8 @@ | 0 => True | S _ => True end = True - ]] *) + ]] + *) reflexivity.