diff options
Diffstat (limited to 'doc/stdlib/Library.tex')
| -rwxr-xr-x | doc/stdlib/Library.tex | 10 |
1 files changed, 6 insertions, 4 deletions
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 $ |