From 6a9642c043e9e41aaed48449151884ad6dcb7050 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 6 Mar 2016 20:36:57 +0100
Subject: [PATCH] docs: improve structure

---
 docs/logic.tex | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/docs/logic.tex b/docs/logic.tex
index 396d3ffc8..7aa98133a 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -74,8 +74,6 @@ Furthermore, $\SigAx$ is a set of \emph{axioms}, that is, terms $\term$ of type
 Again, the grammar of terms and their typing rules are defined below, and depends only on $\SigType$ and $\SigFn$, not on $\SigAx$.
 Elements of $\SigAx$ are ranged over by $\sigax$.
 
-\section{Syntax}
-
 \subsection{Grammar}\label{sec:grammar}
 
 \paragraph{Syntax.}
@@ -276,7 +274,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
 	}
 \end{mathparpagebreakable}
 
-\subsection{Timeless Propositions}
+\subsection{Timeless propositions}
 
 Some propositions are \emph{timeless}, which intuitively means that step-indexing does not affect them.
 This is a \emph{meta-level} assertions about propositions, defined by the following judgment.
@@ -285,7 +283,7 @@ This is a \emph{meta-level} assertions about propositions, defined by the follow
 
 \ralf{Define a judgment that defines them.}
 
-\subsection{Base logic}
+\subsection{Proof rules}
 
 \ralf{Go on checking below.}
 The judgment $\vctx \mid \pfctx \proves \prop$ says that with free variables $\vctx$, proposition $\prop$ holds whenever all assumptions $\pfctx$ hold.
-- 
GitLab