diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-26 17:43:00 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-26 17:43:00 +0000 |
| commit | 8cf5f162214b2161d9242e4b5bf8a81d7ade214e (patch) | |
| tree | d81e69f4f9814f6cb9beb4a0e03d50457e4c75c5 /doc/refman/RefMan-pro.tex | |
| parent | a67ada0c8e569e12430c85ad1847fa313cb5a619 (diff) | |
added doc for declarative language
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9286 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman/RefMan-pro.tex')
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index ddfce775d..a8b7e5459 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: |