From 13dcab5b8f40058b7597e51a44207c0745eab9fd Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 1 Aug 2017 16:46:37 +0200
Subject: Port ssr manual to Coq's latex/hevea style

Work done by Assia Mahboubi and Enrico Tassi
---
 doc/refman/Reference-Manual.tex | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'doc/refman/Reference-Manual.tex')

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
-- 
cgit v1.2.3

