From 55ce117e8083477593cf1ff2e51a3641c7973830 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 13 Feb 2007 13:48:12 +0000 Subject: Imported Upstream version 8.1+dfsg --- doc/refman/AddRefMan-pre.tex | 58 -------------------------------------------- 1 file changed, 58 deletions(-) delete mode 100644 doc/refman/AddRefMan-pre.tex (limited to 'doc/refman/AddRefMan-pre.tex') diff --git a/doc/refman/AddRefMan-pre.tex b/doc/refman/AddRefMan-pre.tex deleted file mode 100644 index 5312b8fc..00000000 --- a/doc/refman/AddRefMan-pre.tex +++ /dev/null @@ -1,58 +0,0 @@ -%\coverpage{Addendum to the Reference Manual}{\ } -%\addcontentsline{toc}{part}{Additional documentation} -\setheaders{Presentation of the Addendum} -\chapter*{Presentation of the Addendum} - -Here you will find several pieces of additional documentation for the -\Coq\ Reference Manual. Each of this chapters is concentrated on a -particular topic, that should interest only a fraction of the \Coq\ -users: that's the reason why they are apart from the Reference -Manual. - -\begin{description} - -\item[Extended pattern-matching] This chapter details the use of - generalized pattern-matching. It is contributed by Cristina Cornes - and Hugo Herbelin. - -\item[Implicit coercions] This chapter details the use of the coercion - mechanism. It is contributed by Amokrane Saïbi. - -%\item[Proof of imperative programs] This chapter explains how to -% prove properties of annotated programs with imperative features. -% It is contributed by Jean-Christophe Filliâtre - -\item[Program extraction] This chapter explains how to extract in practice ML - files from $\FW$ terms. It is contributed by Jean-Christophe - Filliâtre and Pierre Letouzey. - -%\item[Natural] This chapter is due to Yann Coscoy. It is the user -% manual of the tools he wrote for printing proofs in natural -% language. At this time, French and English languages are supported. - -\item[omega] \texttt{omega}, written by Pierre Crégut, solves a whole - class of arithmetic problems. - -%\item[Program] The \texttt{Program} technology intends to inverse the -% extraction mechanism. It allows the developments of certified -% programs in \Coq. This chapter is due to Catherine Parent. {\bf This -% feature is not available in {\Coq} version 7.} - -\item[The {\tt ring} tactic] This is a tactic to do AC rewriting. This - chapter explains how to use it and how it works. - The chapter is contributed by Patrick Loiseleur. - -\item[The {\tt Setoid\_replace} tactic] This is a - tactic to do rewriting on types equipped with specific (only partially - substitutive) equality. The chapter is contributed by Clément Renard. - - -\end{description} - -\atableofcontents - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: -- cgit v1.2.3