diff --git a/tex/ch0.tex b/tex/ch0.tex index 9ae5b402..84cf10cb 100644 --- a/tex/ch0.tex +++ b/tex/ch0.tex @@ -183,6 +183,8 @@ \subsection*{Conventions} like \lib{ssreflect} or \lib{fintype}. \subsection*{Running examples in the \Coq{} system} +\label{ssec:runcoq} + The contents of this book is mostly about interacting with a computer program consisting of the \Coq{} system and the \mcbMC{} library. Many examples are given, and we advise readers to experiment with this program,