Mercurial > cpdt > repo
diff src/Match.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 | f4768d5a75eb |
| children | d5787b70cf48 |
line wrap: on
line diff
--- a/src/Match.v Mon Jan 17 11:42:09 2011 -0500 +++ b/src/Match.v Mon Jan 17 15:12:30 2011 -0500 @@ -129,7 +129,8 @@ (** [[ ============================ g (g (g x)) = g x - ]] *) + ]] + *) Abort. @@ -158,7 +159,8 @@ P (f x) subgoal 4 is: P (f x) - ]] *) + ]] + *) Abort. @@ -414,7 +416,8 @@ H4 : S x ============================ S x - ]] *) + ]] + *) assumption. Qed. @@ -479,7 +482,8 @@ end. User error: No matching clauses for match goal - ]] *) + ]] + *) Abort. (* end thide *) @@ -569,7 +573,8 @@ n := 3 : nat ============================ False - ]] *) + ]] + *) Abort. (* end thide *) @@ -601,7 +606,8 @@ l := (1, 1) :: (2, 2) :: (3, 3) :: nil : list (nat * nat) ============================ False - ]] *) + ]] + *) Abort. (* end thide *) @@ -850,7 +856,8 @@ (Match (P:=P x) (imp_True (P:=True)))))))) : forall (P : nat -> Prop) (Q : Prop), (exists x : nat, P x /\ Q) --> Q /\ (exists x : nat, P x) -]] *) +]] +*) (** * Creating Unification Variables *)