uniformization of capitaliztion in part/section titles

math-comp · Jan 14, 2021 · d34ce52 · d34ce52
1 parent 9b980dc
commit d34ce52
Show file tree

Hide file tree

Showing 8 changed files with 11 additions and 11 deletions.
diff --git a/tex/chProgramming.tex b/tex/chProgramming.tex
@@ -12,7 +12,7 @@
 .
 \end{coqdef}
 
-\chapter{Functions and Computation}\label{ch:prog}
+\chapter{Functions and computation}\label{ch:prog}
 
 In the formalism underlying the \Coq{} system, functions play a
 central role akin to the one of sets in set theory. However,

diff --git a/tex/chProofLanguage.tex b/tex/chProofLanguage.tex
@@ -1,4 +1,4 @@
-\chapter{A Proof Language for Formal Proofs}{}
+\chapter{A proof language for formal proofs}{}
 \label{ch:script}
 
 
@@ -87,7 +87,7 @@ \chapter{A Proof Language for Formal Proofs}{}
 %\section{Managing the proof context}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\section{Bookkeeping: Goals as stacks}\label{ssec:stack}
+\section{Bookkeeping: goals as stacks}\label{ssec:stack}
 \index[concept]{goal stack model}
 
 The presentation we gave so far of proof commands like \C{case: n => [|m]}

diff --git a/tex/chProofs.tex b/tex/chProofs.tex
@@ -31,7 +31,7 @@
 \end{coqdef}
 
 
-\chapter{First Steps in Formal Proofs}{}
+\chapter{First steps in formal proofs}{}
 \label{ch:proofs}
 % In this chapter we explain how to state a lemma,
 % how to prove it, and how to search existing, loaded library.

diff --git a/tex/chSigmaBool.tex b/tex/chSigmaBool.tex
@@ -19,7 +19,7 @@
 Require Import tuple.
 \end{coqdef}
 
-\chapter{Sub-Types}{}\label{ch:sigmabool}
+\chapter{Sub-types}{}\label{ch:sigmabool}
 
 Inductive data types have been used to both code data, like lists, and
 logical connectives, like the existential quantifier.

diff --git a/tex/chSpecification.tex b/tex/chSpecification.tex
@@ -1,4 +1,4 @@
-\chapter{Inductive Specifications}{}
+\chapter{Inductive specifications}{}
 \label{ch:boolrefl}
 
 % in addition to the photos:

diff --git a/tex/chTT.tex b/tex/chTT.tex
@@ -1,4 +1,4 @@
-\chapter{Dependent Type Theory}{}
+\chapter{Dependent type theory}{}
 \label{ch:ttch}
 
 %% Summary of the 22/02 discussion:

diff --git a/tex/chTypeInference.tex b/tex/chTypeInference.tex
@@ -12,7 +12,7 @@
 Abort.
 \end{coqdef}
 
-\chapter{Implicit Parameters}{}
+\chapter{Implicit parameters}{}
 
 The rules of the \mcbCIC{}, as the ones sketched in~\ref{ch:ttch},
 are expressed on the syntax of terms and
@@ -91,7 +91,7 @@ \chapter{Implicit Parameters}{}
 %\mcbLEARN{HO unif is hard}
 %\mcbREQUIRE{}
 %\mcbPROVIDE{terminology}
-\section{Type inference and Higher-Order unification}\label{sec:hounif}
+\section{Type inference and higher-order unification}\label{sec:hounif}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 The type inference algorithm is quite similar to the type checking

diff --git a/tex/main.tex b/tex/main.tex
@@ -58,8 +58,8 @@
 \makeindex[name=coq,title=Definitions and Notations,intoc]
 \makeindex[name=vernac,title=Coq Commands,intoc]
 
-\newcommand{\partonename}{Languages for writing Formal Mathematics}
-\newcommand{\parttwoname}{Crafting a Formal Library}
+\newcommand{\partonename}{Languages for writing formal mathematics}
+\newcommand{\parttwoname}{Crafting a formal library}