--- a/src/StackMachine.v	Fri Nov 06 10:52:43 2009 -0500
+++ b/src/StackMachine.v	Fri Nov 06 12:15:05 2009 -0500
@@ -73,6 +73,8 @@
     | Times => mult
   end.
 
+]]
+
 In this example, we could also omit all of the type annotations, arriving at:
 
 [[
@@ -82,6 +84,8 @@
     | Times => mult
   end.
 
+]]
+
 Languages like Haskell and ML have a convenient %\textit{%#<i>#principal typing#</i>#%}% property, which gives us strong guarantees about how effective type inference will be.  Unfortunately, Coq's type system is so expressive that any kind of "complete" type inference is impossible, and the task even seems to be hard heuristically in practice.  Nonetheless, Coq includes some very helpful heuristics, many of them copying the workings of Haskell and ML type-checkers for programs that fall in simple fragments of Coq's language.
 
 This is as good a time as any to mention the preponderance of different languages associated with Coq.  The theoretical foundation of Coq is a formal system called the %\textit{%#<i>#Calculus of Inductive Constructions (CIC)#</i>#%}%, which is an extension of the older %\textit{%#<i>#Calculus of Constructions (CoC)#</i>#%}%.  CIC is quite a spartan foundation, which is helpful for proving metatheory but not so helpful for real development.  Still, it is nice to know that it has been proved that CIC enjoys properties like %\textit{%#<i>#strong normalization#</i>#%}%, meaning that every program (and, more importantly, every proof term) terminates; and %\textit{%#<i>#relative consistency#</i>#%}% with systems like versions of Zermelo Fraenkel set theory, which roughly means that you can believe that Coq proofs mean that the corresponding propositions are "really true," if you believe in set theory.
@@ -107,17 +111,13 @@
 (** It is convenient to be able to test definitions before starting to prove things about them.  We can verify that our semantics is sensible by evaluating some sample uses. *)
 
 Eval simpl in expDenote (Const 42).
-(** [[
-= 42 : nat
-]] *)
+(** [= 42 : nat] *)
+
 Eval simpl in expDenote (Binop Plus (Const 2) (Const 2)).
-(** [[
-= 4 : nat
-]] *)
+(** [= 4 : nat] *)
+
 Eval simpl in expDenote (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)).
-(** [[
-= 28 : nat
-]] *)
+(** [= 28 : nat] *)
 
 (** ** Target Language *)
 
@@ -277,9 +277,7 @@
 *)
 
   unfold compile.
-
 (** [[
-
  n : nat
  s : stack
  p : list instr
@@ -289,9 +287,7 @@
 ]] *)
 
   unfold expDenote.
-
 (** [[
-
  n : nat
  s : stack
  p : list instr
@@ -463,6 +459,8 @@
 [[
 Proof completed.
 
+]]
+
 And there lies our first proof.  Already, even for simple theorems like this, the final proof script is unstructured and not very enlightening to readers.  If we extend this approach to more serious theorems, we arrive at the unreadable proof scripts that are the favorite complaints of opponents of tactic-based proving.  Fortunately, Coq has rich support for scripted automation, and we can take advantage of such a scripted tactic (defined elsewhere) to make short work of this lemma.  We abort the old proof attempt and start again.
 *)
 
@@ -709,6 +707,8 @@
       end
   end.
 
+]]
+
 The Coq type-checker complains that:
 
 [[