diff options
Diffstat (limited to 'doc/refman/CanonicalStructures.tex')
| -rw-r--r-- | doc/refman/CanonicalStructures.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex index fab660711..28a6f6903 100644 --- a/doc/refman/CanonicalStructures.tex +++ b/doc/refman/CanonicalStructures.tex @@ -38,7 +38,7 @@ Module EQ. End EQ. \end{coq_example} -We use Coq modules as name spaces. This allows to follow the same pattern +We use Coq modules as name spaces. This allows us to follow the same pattern and naming convention for the rest of the chapter. The base name space contains the definitions of the algebraic structure. To keep the example small, the algebraic structure $EQ.type$ we are defining is very simplistic, |