From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 doc/refman/RefMan-pro.tex | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'doc/refman/RefMan-pro.tex')

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 8c1a7824..208a014a 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -374,7 +374,18 @@ All the hypotheses remains usable in the proof development.
 This command goes back to the default mode which is to print all
 available hypotheses.
 
-% $Id: RefMan-pro.tex 9030 2006-07-07 15:37:23Z herbelin $
+\section{$DPL$ : A Declarative proof language for Coq \emph{(experimental)} }
+
+An implementation of the $DPL$ declarative proof language by Pierre Corbineau at the Radboud University Nijmegen (The Netherlands) is included in Coq.
+
+ Due to the experimental nature and hence the potentially unstable semantics of the language, its documentation is not included here. However, it can be found at :
+
+\url{http://www.cs.ru.nl/~corbineau/mmode.html}
+
+
+
+
+% $Id: RefMan-pro.tex 9286 2006-10-26 17:43:00Z corbinea $
 
 %%% Local Variables: 
 %%% mode: latex
-- 
cgit v1.2.3

