diff options
Diffstat (limited to 'doc/refman/RefMan-pro.tex')
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index d0ca097473..593ed771f8 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -402,20 +402,6 @@ 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: |