# HG changeset patch # User Adam Chlipala # Date 1221487537 14400 # Node ID 9bdbc43d510eb21846e7496423c749bebdef7183 # Parent 7021e94dbbec55dba696a8e6ba3b5dd1a8834479 Make Chap. 3 title less grand diff -r 7021e94dbbec -r 9bdbc43d510e src/InductiveTypes.v --- a/src/InductiveTypes.v Sat Sep 13 14:35:14 2008 -0400 +++ b/src/InductiveTypes.v Mon Sep 15 10:05:37 2008 -0400 @@ -16,7 +16,7 @@ (* end hide *) -(** %\chapter{Inductive Types}% *) +(** %\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 in Coq and shares some "design patterns" for overcoming common pitfalls with them. *) diff -r 7021e94dbbec -r 9bdbc43d510e src/Intro.v --- a/src/Intro.v Sat Sep 13 14:35:14 2008 -0400 +++ b/src/Intro.v Mon Sep 15 10:05:37 2008 -0400 @@ -185,7 +185,7 @@ \hline Some Quick Examples & \texttt{StackMachine.v} \\ \hline -Inductive Types & \texttt{InductiveTypes.v} \\ +Introducing Inductive Types & \texttt{InductiveTypes.v} \\ \hline \end{tabular} \end{center}