Index: doc/theses/fangren_yu_MMath/background.tex
===================================================================
--- doc/theses/fangren_yu_MMath/background.tex	(revision 68c706218a8f56600244dd3a5720da31f8655420)
+++ doc/theses/fangren_yu_MMath/background.tex	(revision bea0291a76a02eb8c6e8f7f6a0e9f8f6bd95cabe)
@@ -68,5 +68,5 @@
 
 
-\section{Type resolution}
+\section{Type Resolution}
 
 \CFA expression resolution must deal with extensive overloading and inference of polymorphic types with assertions.
Index: doc/theses/fangren_yu_MMath/future.tex
===================================================================
--- doc/theses/fangren_yu_MMath/future.tex	(revision 68c706218a8f56600244dd3a5720da31f8655420)
+++ doc/theses/fangren_yu_MMath/future.tex	(revision bea0291a76a02eb8c6e8f7f6a0e9f8f6bd95cabe)
@@ -6,5 +6,5 @@
 
 
-\section{Closed trait types}
+\section{Closed Trait Types}
 
 Currently, \CFA does not have any closed types, as open type are the basis of its unique type-system, allowing new functions to be added at any time to override existing ones for trait satisfaction.
@@ -157,5 +157,5 @@
 
 
-\section{User-defined conversions}
+\section{User-defined Conversions}
 
 Missing type-system feature is a scheme for user-defined conversions.