From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- doc/stdlib/Library.tex | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'doc/stdlib/Library.tex') diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex index 598943a4..f9764bea 100755 --- a/doc/stdlib/Library.tex +++ b/doc/stdlib/Library.tex @@ -3,7 +3,7 @@ \usepackage[latin1]{inputenc} \usepackage[T1]{fontenc} \usepackage{fullpage} -\usepackage{coqdoc} +\usepackage{../../coqdoc} \input{../common/version} \input{../common/title} @@ -43,8 +43,10 @@ The standard library is composed of the following subdirectories: \item[Sorting] Sorted list (basic definitions and heapsort correctness). \item[Wellfounded] Well-founded relations (basic results). - \item[IntMap] Representation of finite sets by an efficient - structure of map (trees indexed by binary integers). + \item[Program] Tactics to deal with dependently-typed programs and + their proofs. + \item[Classes] Standard type class instances on relations and + Coq part of the setoid rewriting tactic. \end{description} @@ -59,4 +61,4 @@ you can access from the \Coq\ home page at \end{document} -% $Id: Library.tex 9245 2006-10-17 12:53:34Z notin $ +% $Id: Library.tex 11091 2008-06-10 18:24:52Z notin $ -- cgit v1.2.3