diff options
| author | Maxime Dénès | 2017-08-16 09:51:16 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-16 09:51:16 +0200 |
| commit | 4b92a109d0d8e1f04e259f56d82b5d15b3c79134 (patch) | |
| tree | d08cf96208a2aa572cb354cb3f5f8cb4c8edf01b /doc/refman/Reference-Manual.tex | |
| parent | e1264c9f0d50bf8ca09fa7388101daa0b4c29635 (diff) | |
| parent | 82fe61d1ec6969be6dc32ae3006faf99c8eedd55 (diff) | |
Merge PR #831: Port ssreflect user manual to Coq's latex/hevea style
Diffstat (limited to 'doc/refman/Reference-Manual.tex')
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 291c07de4c..fc1c01cf24 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -22,6 +22,17 @@ \usepackage{xspace} \usepackage{pmboxdraw} \usepackage{float} +\usepackage{color} + \definecolor{dkblue}{rgb}{0,0.1,0.5} + \definecolor{lightblue}{rgb}{0,0.5,0.5} + \definecolor{dkgreen}{rgb}{0,0.4,0} + \definecolor{dk2green}{rgb}{0.4,0,0} + \definecolor{dkviolet}{rgb}{0.6,0,0.8} + \definecolor{dkpink}{rgb}{0.2,0,0.6} +\usepackage{listings} + \def\lstlanguagefiles{coq-listing.tex} +\usepackage{tabularx} +\usepackage{array,longtable} \floatstyle{boxed} \restylefloat{figure} @@ -99,6 +110,11 @@ Options A and B of the licence are {\em not} elected.} \include{RefMan-ltac.v}% Writing tactics \include{RefMan-tacex.v}% Detailed Examples of tactics +\lstset{language=SSR} +\lstset{moredelim=[is][]{|*}{*|}} +\lstset{moredelim=*[is][\itshape\rmfamily]{/*}{*/}} +\include{RefMan-ssr} + \part{User extensions} \include{RefMan-syn.v}% The Syntax and the Grammar commands %%SUPPRIME \include{RefMan-tus.v}% Writing tactics |