From 8cf5f162214b2161d9242e4b5bf8a81d7ade214e Mon Sep 17 00:00:00 2001
From: corbinea
Date: Thu, 26 Oct 2006 17:43:00 +0000
Subject: added doc for declarative language

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9286 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-pro.tex | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index ddfce775dd..a8b7e5459a 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -374,6 +374,17 @@ All the hypotheses remains usable in the proof development.
 This command goes back to the default mode which is to print all
 available hypotheses.
 
+\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$
 
 %%% Local Variables: 
-- 
cgit v1.2.3