# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1223058561 14400
# Node ID a21447f76aadac7c75db4d546159f920906a77d4
# Parent  535e1cd17d9a40e0b20d07fa35827c2fe32894a2
Break into Parts

diff -r 535e1cd17d9a -r a21447f76aad src/InductiveTypes.v
--- a/src/InductiveTypes.v	Fri Oct 03 14:14:28 2008 -0400
+++ b/src/InductiveTypes.v	Fri Oct 03 14:29:21 2008 -0400
@@ -16,7 +16,9 @@
 (* end hide *)
 
 
-(** %\chapter{Introducing Inductive Types}% *)
+(** %\part{Basic Programming and Proving}
+
+\chapter{Introducing Inductive Types}% *)
 
 (** In a sense, CIC is built from just two relatively straightforward features: function types and inductive types.  From this modest foundation, we can prove effectively all of the theorems of math and carry out effectively all program verifications, with enough effort expended.  This chapter introduces induction and recursion for functional programming in Coq. *)
 
diff -r 535e1cd17d9a -r a21447f76aad src/Subset.v
--- a/src/Subset.v	Fri Oct 03 14:14:28 2008 -0400
+++ b/src/Subset.v	Fri Oct 03 14:29:21 2008 -0400
@@ -16,7 +16,9 @@
 (* end hide *)
 
 
-(** %\chapter{Subset Types and Variations}% *)
+(** %\part{Programming with Dependent Types}
+
+\chapter{Subset Types and Variations}% *)
 
 (** So far, we have seen many examples of what we might call "classical program verification."  We write programs, write their specifications, and then prove that the programs satisfy their specifications.  The programs that we have written in Coq have been normal functional programs that we could just as well have written in Haskell or ML.  In this chapter, we start investigating uses of %\textit{%#<i>#dependent types#</i>#%}% to integrate programming, specification, and proving into a single phase. *)
 
@@ -569,10 +571,6 @@
 Eval simpl in typeCheck (Plus (Nat 1) (Nat 2)).
 Eval simpl in typeCheck (Plus (Nat 1) (Bool false)).
 
-Print sumor.
-
-
-
 Notation "e1 ;;; e2" := (if e1 then e2 else !!)
   (right associativity, at level 60).