diff options
Diffstat (limited to 'doc/refman/RefMan-syn.tex')
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index d8a353300..eecb5ac7c 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -1,4 +1,5 @@ \chapter[Syntax extensions and interpretation scopes]{Syntax extensions and interpretation scopes\label{Addoc-syntax}} +%HEVEA\cutname{syntax-extensions.html} In this chapter, we introduce advanced commands to modify the way {\Coq} parses and prints objects, i.e. the translations between the |