Mercurial > cpdt > repo

diff src/StackMachine.v @ 302:7b38729be069

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 f7ac1e0c0d60
line wrap: on
line diff
--- a/src/StackMachine.v	Mon Jan 17 11:42:09 2011 -0500
+++ b/src/StackMachine.v	Mon Jan 17 15:12:30 2011 -0500
@@ -311,9 +311,11 @@
  progDenote ((IConst n :: nil) ++ p) s =
  progDenote p (expDenote (Const n) :: s)
  
-]] *)
+]]
+*)
 
   unfold expDenote.
+
 (** [[
  n : nat
  s : stack
@@ -529,7 +531,8 @@
 (** [[
 app_nil_end
      : forall (A : Type) (l : list A), l = l ++ nil
-]] *)
+]]
+*)
 
   rewrite (app_nil_end (compile e)).
 
@@ -827,7 +830,8 @@
            (TCons (TIBinop ts b) (TNil (res :: ts))))
   end
      : forall t : type, texp t -> forall ts : tstack, tprog ts (t :: ts)
-]] *)
+]]
+*)
 
 
 (** We can check that the compiler generates programs that behave appropriately on our sample programs from above: *)