### changeset 269:191a66cd7cb5

Fix PDF ToC generation; mention Set Implicit Arguments in StackMachine
author Adam Chlipala Wed, 03 Feb 2010 08:14:39 -0500 f3223bde5c87 fd46d077b952 src/Intro.v src/StackMachine.v 2 files changed, 5 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/Intro.v	Wed Jan 27 07:40:03 2010 -0500
+++ b/src/Intro.v	Wed Feb 03 08:14:39 2010 -0500
@@ -9,6 +9,8 @@

(** %\fi

+\usepackage{hyperref}
+
\begin{document}

\maketitle
@@ -33,6 +35,7 @@
(** %\vfill\mbox{}
\end{center}

+\phantomsection
\tableofcontents

\chapter{Introduction}% *)
--- a/src/StackMachine.v	Wed Jan 27 07:40:03 2010 -0500
+++ b/src/StackMachine.v	Wed Feb 03 08:14:39 2010 -0500
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2009, Adam Chlipala
+(* Copyright (c) 2008-2010, Adam Chlipala
*
* This work is licensed under a
* Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -21,7 +21,7 @@

(** I will start off by jumping right in to a fully-worked set of examples, building certified compilers from increasingly complicated source languages to stack machines.  We will meet a few useful tactics and see how they can be used in manual proofs, and we will also see how easily these proofs can be automated instead.  I assume that you have installed Coq and Proof General.  The code in this book is tested with Coq version 8.2pl1, though parts may work with other versions.

-As always, you can step through the source file %\texttt{%#<tt>#StackMachine.v#</tt>#%}% for this chapter interactively in Proof General.  Alternatively, to get a feel for the whole lifecycle of creating a Coq development, you can enter the pieces of source code in this chapter in a new %\texttt{%#<tt>#.v#</tt>#%}% file in an Emacs buffer.  If you do the latter, include a line [Require Import List Tactics.] at the start of the file, to match some code hidden in this rendering of the chapter source, and be sure to run the Coq binary %\texttt{%#<tt>#coqtop#</tt>#%}% with the command-line argument %\texttt{%#<tt>#-I SRC#</tt>#%}%, where %\texttt{%#<tt>#SRC#</tt>#%}% is the path to a directory containing the source for this book.  In either case, you will need to run %\texttt{%#<tt>#make#</tt>#%}% in the root directory of the source distribution for the book before getting started.  If you have installed Proof General properly, it should start automatically when you visit a %\texttt{%#<tt>#.v#</tt>#%}% buffer in Emacs.
+As always, you can step through the source file %\texttt{%#<tt>#StackMachine.v#</tt>#%}% for this chapter interactively in Proof General.  Alternatively, to get a feel for the whole lifecycle of creating a Coq development, you can enter the pieces of source code in this chapter in a new %\texttt{%#<tt>#.v#</tt>#%}% file in an Emacs buffer.  If you do the latter, include two lines [Require Import List Tactics.] and [Set Implicit Arguments.] at the start of the file, to match some code hidden in this rendering of the chapter source, and be sure to run the Coq binary %\texttt{%#<tt>#coqtop#</tt>#%}% with the command-line argument %\texttt{%#<tt>#-I SRC#</tt>#%}%, where %\texttt{%#<tt>#SRC#</tt>#%}% is the path to a directory containing the source for this book.  In either case, you will need to run %\texttt{%#<tt>#make#</tt>#%}% in the root directory of the source distribution for the book before getting started.  If you have installed Proof General properly, it should start automatically when you visit a %\texttt{%#<tt>#.v#</tt>#%}% buffer in Emacs.

There are some minor headaches associated with getting Proof General to pass the proper command line arguments to the %\texttt{%#<tt>#coqtop#</tt>#%}% program.  The best way to add settings that will be shared by many source files is to add a custom variable setting to your %\texttt{%#<tt>#.emacs#</tt>#%}% file, like this:
%\begin{verbatim}%#<pre>#(custom-set-variables