From 72c35b310a7b8a23934a1e9632d4d989c184d0d7 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 16 Apr 2018 18:16:37 +0200 Subject: Remove LaTeX refman, now that migration to Sphinx is complete --- .gitignore | 18 - INSTALL.doc | 4 +- Makefile | 5 +- Makefile.doc | 129 +--- doc/refman/AddRefMan-pre.tex | 63 -- doc/refman/Reference-Manual.tex | 134 ---- doc/refman/biblio.bib | 1397 --------------------------------------- doc/refman/coq-listing.tex | 152 ----- doc/refman/coqide-queries.png | Bin 66656 -> 0 bytes doc/refman/coqide.png | Bin 59662 -> 0 bytes doc/refman/headers.hva | 44 -- doc/refman/headers.sty | 88 --- doc/refman/index.html | 14 - doc/refman/menu.html | 32 - 14 files changed, 12 insertions(+), 2068 deletions(-) delete mode 100644 doc/refman/AddRefMan-pre.tex delete mode 100644 doc/refman/Reference-Manual.tex delete mode 100644 doc/refman/biblio.bib delete mode 100644 doc/refman/coq-listing.tex delete mode 100644 doc/refman/coqide-queries.png delete mode 100644 doc/refman/coqide.png delete mode 100644 doc/refman/headers.hva delete mode 100644 doc/refman/headers.sty delete mode 100644 doc/refman/index.html delete mode 100644 doc/refman/menu.html diff --git a/.gitignore b/.gitignore index 267534365..25c0996cb 100644 --- a/.gitignore +++ b/.gitignore @@ -96,21 +96,6 @@ doc/faq/axioms.eps doc/faq/axioms.eps_t doc/faq/axioms.pdf_t doc/faq/axioms.png -doc/refman/.csdp.cache -doc/refman/trace -doc/refman/Reference-Manual.ps -doc/refman/Reference-Manual.html -doc/refman/Reference-Manual.out -doc/refman/Reference-Manual.sh -doc/refman/cover.html -doc/refman/styles.hva -doc/refman/coqide-queries.eps -doc/refman/coqide.eps -doc/refman/euclid.ml -doc/refman/euclid.mli -doc/refman/heapsort.ml -doc/refman/heapsort.mli -doc/refman/html/ doc/stdlib/Library.out doc/stdlib/Library.ps doc/stdlib/Library.coqdoc.tex @@ -177,9 +162,6 @@ dev/myinclude # coqide generated files (when testing) *.crashcoqide -/doc/refman/Reference-Manual.hoptind -/doc/refman/Reference-Manual.optidx -/doc/refman/Reference-Manual.optind user-contrib .*.sw* diff --git a/INSTALL.doc b/INSTALL.doc index b71115bfa..b424f9f64 100644 --- a/INSTALL.doc +++ b/INSTALL.doc @@ -66,8 +66,8 @@ Alternatively, you can use some specific targets: make doc-html to produce all html documents - make refman - to produce all formats of the reference manual + make sphinx + to produce the HTML version of the reference manual make tutorial to produce all formats of the tutorial diff --git a/Makefile b/Makefile index c31534f36..793afb661 100644 --- a/Makefile +++ b/Makefile @@ -235,11 +235,8 @@ docclean: doc/stdlib/*Library.coqdoc.tex doc/stdlib/library.files \ doc/stdlib/library.files.ls doc/stdlib/FullLibrary.tex rm -f doc/*/*.ps doc/*/*.pdf doc/*/*.eps doc/*/*.pdf_t doc/*/*.eps_t - rm -rf doc/refman/html doc/stdlib/html doc/tutorial/tutorial.v.html - rm -f doc/refman/euclid.ml doc/refman/euclid.mli - rm -f doc/refman/heapsort.ml doc/refman/heapsort.mli + rm -rf doc/stdlib/html doc/tutorial/tutorial.v.html rm -f doc/common/version.tex - rm -f doc/refman/styles.hva doc/refman/cover.html doc/refman/Reference-Manual.html rm -f doc/coq.tex rm -rf doc/sphinx/_build diff --git a/Makefile.doc b/Makefile.doc index dc2b9f55d..ce31c5fcb 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -56,29 +56,14 @@ ALLSPHINXOPTS= -d $(SPHINXBUILDDIR)/doctrees $(SPHINXOPTS) DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex -REFMANCOQTEXFILES:=$(addprefix doc/refman/, ) - -REFMANTEXFILES:=$(addprefix doc/refman/, \ - headers.sty Reference-Manual.tex) \ - $(REFMANCOQTEXFILES) \ - -REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps - -REFMANFILES:=$(REFMANTEXFILES) $(DOCCOMMON) $(REFMANEPSFILES) doc/refman/biblio.bib - -REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png) - - ###################################################################### ### General rules ###################################################################### -.PHONY: doc sphinxdoc-html doc-pdf doc-ps refman refman-quick tutorial -.PHONY: stdlib full-stdlib rectutorial refman-html-dir +.PHONY: doc sphinxdoc-html doc-pdf doc-ps tutorial +.PHONY: stdlib full-stdlib rectutorial -INDEXURLS:=doc/refman/html/index_urls.txt - -doc: sphinx refman tutorial rectutorial stdlib $(INDEXURLS) +doc: sphinx tutorial rectutorial stdlib sphinx: coq $(SHOW)'SPHINXBUILD doc/sphinx' @@ -87,20 +72,17 @@ sphinx: coq @echo "Build finished. The HTML pages are in $(SPHINXBUILDDIR)/html." doc-html:\ - doc/tutorial/Tutorial.v.html doc/refman/html/index.html \ + doc/tutorial/Tutorial.v.html \ doc/stdlib/html/index.html doc/RecTutorial/RecTutorial.html doc-pdf:\ - doc/tutorial/Tutorial.v.pdf doc/refman/Reference-Manual.pdf \ + doc/tutorial/Tutorial.v.pdf \ doc/stdlib/Library.pdf doc/RecTutorial/RecTutorial.pdf doc-ps:\ - doc/tutorial/Tutorial.v.ps doc/refman/Reference-Manual.ps \ + doc/tutorial/Tutorial.v.ps \ doc/stdlib/Library.ps doc/RecTutorial/RecTutorial.ps -refman: \ - doc/refman/html/index.html doc/refman/Reference-Manual.ps doc/refman/Reference-Manual.pdf - tutorial: \ doc/tutorial/Tutorial.v.html doc/tutorial/Tutorial.v.ps doc/tutorial/Tutorial.v.pdf @@ -158,82 +140,6 @@ SHOWMAKEINDEXERROR=egrep '^!! Input index error|^\*\* Input style error|^ --' doc/common/version.tex: config/Makefile printf '\\newcommand{\\coqversion}{$(VERSION)}' > doc/common/version.tex -###################################################################### -# Reference Manual -###################################################################### - - -### Reference Manual (printable format) - -# The second LATEX compilation is necessary otherwise the pages of the index -# are not correct (don't know why...) - BB -doc/refman/Reference-Manual.dvi: $(REFMANFILES) doc/refman/Reference-Manual.tex - @(cd doc/refman;\ - $(LATEX) -interaction=batchmode Reference-Manual;\ - $(BIBTEX) -terse Reference-Manual $(HIDEBIBTEXINFO);\ - $(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\ - $(MAKEINDEX) -q Reference-Manual;\ - $(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\ - $(MAKEINDEX) -q Reference-Manual.tacidx -o Reference-Manual.tacind;\ - $(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\ - $(MAKEINDEX) -q Reference-Manual.comidx -o Reference-Manual.comind;\ - $(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\ - $(MAKEINDEX) -q Reference-Manual.optidx -o Reference-Manual.optind;\ - $(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\ - $(MAKEINDEX) -q Reference-Manual.erridx -o Reference-Manual.errind;\ - $(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\ - $(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\ - $(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\ - ../tools/show_latex_messages -no-overfull Reference-Manual.log) - -doc/refman/Reference-Manual.pdf: doc/refman/Reference-Manual.dvi $(REFMANPNGFILES) - (cd doc/refman;\ - $(PDFLATEX) -interaction=batchmode Reference-Manual.tex;\ - ../tools/show_latex_messages -no-overfull Reference-Manual.log) - -### Reference Manual (browsable format) - -doc/refman/Reference-Manual.html: doc/refman/styles.hva doc/refman/headers.hva doc/refman/Reference-Manual.dvi # to ensure bbl file - (cd doc/refman; BIBINPUTS=.: $(HEVEA) $(HEVEAOPTS) ./styles.hva ./Reference-Manual.tex) - -doc/refman/cover.html: doc/common/styles/html/$(HTMLSTYLE)/cover.html - sed -e "s/COQVERSION/$(VERSION)/g" $< > $@ - -doc/refman/styles.hva: doc/common/styles/html/$(HTMLSTYLE)/styles.hva - $(INSTALLLIB) $< doc/refman - -INDEXES:= doc/refman/html/command-index.html doc/refman/html/tactic-index.html - -refman-html-dir $(INDEXES): doc/refman/html/index.html ; - -doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \ - doc/refman/cover.html doc/refman/styles.hva doc/refman/index.html - - rm -rf doc/refman/html - $(MKDIR) doc/refman/html - $(INSTALLLIB) $(REFMANPNGFILES) doc/refman/html - (cd doc/refman/html; $(HACHA) -nolinks -tocbis -o toc.html ../styles.hva ../Reference-Manual.html) - $(INSTALLLIB) doc/refman/cover.html doc/refman/html/index.html - @touch $(INDEXES) - (cd doc/common/styles/html/$(HTMLSTYLE);\ - for f in `find . -name \*.css`; do \ - $(MKDIR) $$(dirname ../../../../refman/html/$$f);\ - $(INSTALLLIB) $$f ../../../../refman/html/$$f;\ - done) - -refman-quick: - (cd doc/refman;\ - $(PDFLATEX) -interaction=batchmode Reference-Manual.tex;\ - ../tools/show_latex_messages -no-overfull Reference-Manual.log && \ - $(HEVEA) $(HEVEAOPTS) ./Reference-Manual.tex) - -###################################################################### -# Index file for CoqIDE -###################################################################### - -$(INDEXURLS): $(INDEXES) - cat $< | grep li-indexenv | grep href= | sed -e 's@.*>\([^<]*\).*, .*@\1,\2@' > $@ - - ###################################################################### # Tutorial ###################################################################### @@ -359,30 +265,20 @@ install-doc-meta: $(INSTALLLIB) doc/LICENSE $(FULLDOCDIR)/LICENSE.doc install-doc-html: - $(MKDIR) $(addprefix $(FULLDOCDIR)/html/, refman stdlib) - (for f in `cd doc/refman/html; find . -type f`; do \ - $(MKDIR) $$(dirname $(FULLDOCDIR)/html/refman/$$f);\ - $(INSTALLLIB) doc/refman/html/$$f $(FULLDOCDIR)/html/refman/$$f;\ - done) + $(MKDIR) $(FULLDOCDIR)/html/stdlib $(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib $(INSTALLLIB) doc/RecTutorial/RecTutorial.html $(FULLDOCDIR)/html/RecTutorial.html $(INSTALLLIB) doc/tutorial/Tutorial.v.html $(FULLDOCDIR)/html/Tutorial.html install-doc-printable: $(MKDIR) $(FULLDOCDIR)/ps $(FULLDOCDIR)/pdf - $(INSTALLLIB) doc/refman/Reference-Manual.pdf \ - doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf - $(INSTALLLIB) doc/refman/Reference-Manual.ps \ - doc/stdlib/Library.ps $(FULLDOCDIR)/ps + $(INSTALLLIB) doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf + $(INSTALLLIB) doc/stdlib/Library.ps $(FULLDOCDIR)/ps $(INSTALLLIB) doc/tutorial/Tutorial.v.pdf $(FULLDOCDIR)/pdf/Tutorial.pdf $(INSTALLLIB) doc/RecTutorial/RecTutorial.pdf $(FULLDOCDIR)/pdf/RecTutorial.pdf $(INSTALLLIB) doc/tutorial/Tutorial.v.ps $(FULLDOCDIR)/ps/Tutorial.ps $(INSTALLLIB) doc/RecTutorial/RecTutorial.ps $(FULLDOCDIR)/ps/RecTutorial.ps -install-doc-index-urls: - $(MKDIR) $(FULLDATADIR) - $(INSTALLLIB) $(INDEXURLS) $(FULLDATADIR) - install-doc-sphinx: $(MKDIR) $(FULLDOCDIR)/sphinx (for f in `cd doc/sphinx/_build; find . -type f`; do \ @@ -467,13 +363,6 @@ $(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex $(HIDE)(cd $(OCAMLDOCDIR) ; pdflatex -interaction=batchmode $*.tex && pdflatex -interaction=batchmode $*.tex) $(HIDE)(cd doc/tools/; ./show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log) -########################################################################### -# local web server -########################################################################### - -serve-refman-8080: refman - cd doc/refman/html; python3 -m http.server 8080 - # For emacs: # Local Variables: # mode: makefile diff --git a/doc/refman/AddRefMan-pre.tex b/doc/refman/AddRefMan-pre.tex deleted file mode 100644 index 856a823de..000000000 --- a/doc/refman/AddRefMan-pre.tex +++ /dev/null @@ -1,63 +0,0 @@ -%\coverpage{Addendum to the Reference Manual}{\ } -%\addcontentsline{toc}{part}{Additional documentation} -%BEGIN LATEX -\setheaders{Presentation of the Addendum} -%END LATEX -\chapter*{Presentation of the Addendum} -%HEVEA\cutname{addendum.html} - -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[Program] This chapter explains the use of the \texttt{Program} - vernacular which allows the development of certified - programs in \Coq. It is contributed by Matthieu Sozeau and replaces - the previous \texttt{Program} tactic by Catherine Parent. - -%\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[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. - -\item[Calling external provers] This chapter describes several tactics - which call external provers. - -\end{description} - -\atableofcontents - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex deleted file mode 100644 index ba4018d77..000000000 --- a/doc/refman/Reference-Manual.tex +++ /dev/null @@ -1,134 +0,0 @@ -%\RequirePackage{ifpdf} -%\ifpdf -% \documentclass[11pt,a4paper,pdftex]{book} -%\else - \documentclass[11pt,a4paper]{book} -%\fi - -\usepackage[utf8]{inputenc} -\usepackage[T1]{fontenc} -\usepackage{textcomp} -\usepackage{times} -\usepackage{url} -\usepackage{verbatim} -\usepackage{amsmath} -\usepackage{amssymb} -\usepackage{alltt} -\usepackage{hevea} -\usepackage{ifpdf} -\usepackage[headings]{fullpage} -\usepackage{headers} % in this directory -\usepackage{multicol} -\usepackage{xspace} -\usepackage{pmboxdraw} -\usepackage{float} -\usepackage{color} - \definecolor{dkblue}{rgb}{0,0.1,0.5} - \definecolor{lightblue}{rgb}{0,0.5,0.5} - \definecolor{dkgreen}{rgb}{0,0.4,0} - \definecolor{dk2green}{rgb}{0.4,0,0} - \definecolor{dkviolet}{rgb}{0.6,0,0.8} - \definecolor{dkpink}{rgb}{0.2,0,0.6} -\usepackage{listings} - \def\lstlanguagefiles{coq-listing.tex} -\usepackage{tabularx} -\usepackage{array,longtable} - -\floatstyle{boxed} -\restylefloat{figure} - -% for coqide -\ifpdf % si on est pas en pdflatex - \usepackage[pdftex]{graphicx} -\else - \usepackage[dvips]{graphicx} -\fi - - -%\includeonly{Setoid} - -\input{../common/version.tex} -\input{../common/macros.tex}% extension .tex pour htmlgen -\input{../common/title.tex}% extension .tex pour htmlgen -%\input{headers} - -\usepackage[linktocpage,colorlinks,bookmarks=true,bookmarksnumbered=true]{hyperref} -% The manual advises to load hyperref package last to be able to redefine -% necessary commands. -% The above should work for both latex and pdflatex. Even if PDF is produced -% through DVI and PS using dvips and ps2pdf, hyperlinks should still work. -% linktocpage option makes page numbers, not section names, to be links in -% the table of contents. -% colorlinks option colors the links instead of using boxes. - -% The command \tocnumber was added to HEVEA in version 1.06-6. -% It instructs HEVEA to put chapter numbers into the table of -% content entries. The table of content is produced by HACHA using -% the options -tocbis -o toc.html. HEVEA produces a warning when -% a command is not recognized, so versions earlier than 1.06-6 can -% still be used. -%HEVEA\tocnumber - -\begin{document} -%BEGIN LATEX -\sloppy\hbadness=5000 -%END LATEX - -%BEGIN LATEX -\coverpage{Reference Manual} -{The Coq Development Team} -{This material may be distributed only subject to the terms and -conditions set forth in the Open Publication License, v1.0 or later -(the latest version is presently available at -\url{http://www.opencontent.org/openpub}). -Options A and B of the licence are {\em not} elected.} -%END LATEX - -%\defaultheaders - -%BEGIN LATEX -\tableofcontents -%END LATEX - -\part{The language} -%BEGIN LATEX -\defaultheaders -%END LATEX - - -\part{The proof engine} -\include{RefMan-ltac.v}% Writing tactics - -\lstset{language=SSR} -\lstset{moredelim=[is][]{|*}{*|}} -\lstset{moredelim=*[is][\itshape\rmfamily]{/*}{*/}} - -%BEGIN LATEX -\RefManCutCommand{BEGINADDENDUM=\thepage} -%END LATEX -\part{Addendum to the Reference Manual} -\include{AddRefMan-pre}% -%BEGIN LATEX -\RefManCutCommand{ENDADDENDUM=\thepage} -%END LATEX -\nocite{*} -\bibliographystyle{plain} -\bibliography{biblio} -\cutname{biblio.html} - -\printrefmanindex{default}{Global Index}{general-index.html} -\printrefmanindex{tactic}{Tactics Index}{tactic-index.html} -\printrefmanindex{command}{Vernacular Commands Index}{command-index.html} -\printrefmanindex{option}{Vernacular Options Index}{option-index.html} -\printrefmanindex{error}{Index of Error Messages}{error-index.html} - -%BEGIN LATEX -\cleardoublepage -\phantomsection -\addcontentsline{toc}{chapter}{\listfigurename} -\listoffigures -%END LATEX - -\end{document} - - diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib deleted file mode 100644 index e69725838..000000000 --- a/doc/refman/biblio.bib +++ /dev/null @@ -1,1397 +0,0 @@ -@String{jfp = "Journal of Functional Programming"} -@String{lncs = "Lecture Notes in Computer Science"} -@String{lnai = "Lecture Notes in Artificial Intelligence"} -@String{SV = "{Sprin-ger-Verlag}"} - -@InProceedings{Aud91, - author = {Ph. Audebaud}, - booktitle = {Proceedings of the sixth Conf. on Logic in Computer Science.}, - publisher = {IEEE}, - title = {Partial {Objects} in the {Calculus of Constructions}}, - year = {1991} -} - -@PhDThesis{Aud92, - author = {Ph. Audebaud}, - school = {{Universit\'e} Bordeaux I}, - title = {Extension du Calcul des Constructions par Points fixes}, - year = {1992} -} - -@InProceedings{Audebaud92b, - author = {Ph. Audebaud}, - booktitle = {{Proceedings of the 1992 Workshop on Types for Proofs and Programs}}, - editor = {{B. Nordstr\"om and K. Petersson and G. Plotkin}}, - note = {Also Research Report LIP-ENS-Lyon}, - pages = {21--34}, - title = {{CC+ : an extension of the Calculus of Constructions with fixpoints}}, - year = {1992} -} - -@InProceedings{Augustsson85, - author = {L. Augustsson}, - title = {{Compiling Pattern Matching}}, - booktitle = {Conference Functional Programming and -Computer Architecture}, - year = {1985} -} - -@Article{BaCo85, - author = {J.L. Bates and R.L. Constable}, - journal = {ACM transactions on Programming Languages and Systems}, - title = {Proofs as {Programs}}, - volume = {7}, - year = {1985} -} - -@Book{Bar81, - author = {H.P. Barendregt}, - publisher = {North-Holland}, - title = {The Lambda Calculus its Syntax and Semantics}, - year = {1981} -} - -@TechReport{Bar91, - author = {H. Barendregt}, - institution = {Catholic University Nijmegen}, - note = {In Handbook of Logic in Computer Science, Vol II}, - number = {91-19}, - title = {Lambda {Calculi with Types}}, - year = {1991} -} - -@Article{BeKe92, - author = {G. Bellin and J. Ketonen}, - journal = {Theoretical Computer Science}, - pages = {115--142}, - title = {A decision procedure revisited : Notes on direct logic, linear logic and its implementation}, - volume = {95}, - year = {1992} -} - -@Book{Bee85, - author = {M.J. Beeson}, - publisher = SV, - title = {Foundations of Constructive Mathematics, Metamathematical Studies}, - year = {1985} -} - -@Book{Bis67, - author = {E. Bishop}, - publisher = {McGraw-Hill}, - title = {Foundations of Constructive Analysis}, - year = {1967} -} - -@Book{BoMo79, - author = {R.S. Boyer and J.S. Moore}, - key = {BoMo79}, - publisher = {Academic Press}, - series = {ACM Monograph}, - title = {A computational logic}, - year = {1979} -} - -@MastersThesis{Bou92, - author = {S. Boutin}, - month = sep, - school = {{Universit\'e Paris 7}}, - title = {Certification d'un compilateur {ML en Coq}}, - year = {1992} -} - -@InProceedings{Bou97, - title = {Using reflection to build efficient and certified decision procedure -s}, - author = {S. Boutin}, - booktitle = {TACS'97}, - editor = {Martin Abadi and Takahashi Ito}, - publisher = SV, - series = lncs, - volume = 1281, - year = {1997} -} - -@PhDThesis{Bou97These, - author = {S. Boutin}, - title = {R\'eflexions sur les quotients}, - school = {Paris 7}, - year = 1997, - type = {th\`ese d'Universit\'e}, - month = apr -} - -@Article{Bru72, - author = {N.J. de Bruijn}, - journal = {Indag. Math.}, - title = {{Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem}}, - volume = {34}, - year = {1972} -} - - -@InCollection{Bru80, - author = {N.J. de Bruijn}, - booktitle = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.}, - editor = {J.P. Seldin and J.R. Hindley}, - publisher = {Academic Press}, - title = {A survey of the project {Automath}}, - year = {1980} -} - -@TechReport{COQ93, - author = {G. Dowek and A. Felty and H. Herbelin and G. Huet and C. Murthy and C. Parent and C. Paulin-Mohring and B. Werner}, - institution = {INRIA}, - month = may, - number = {154}, - title = {{The Coq Proof Assistant User's Guide Version 5.8}}, - year = {1993} -} - -@TechReport{COQ02, - author = {The Coq Development Team}, - institution = {INRIA}, - month = Feb, - number = {255}, - title = {{The Coq Proof Assistant Reference Manual Version 7.2}}, - year = {2002} -} - -@TechReport{CPar93, - author = {C. Parent}, - institution = {Ecole {Normale} {Sup\'erieure} de {Lyon}}, - month = oct, - note = {Also in~\cite{Nijmegen93}}, - number = {93-29}, - title = {Developing certified programs in the system {Coq}- {The} {Program} tactic}, - year = {1993} -} - -@PhDThesis{CPar95, - author = {C. Parent}, - school = {Ecole {Normale} {Sup\'erieure} de {Lyon}}, - title = {{Synth\`ese de preuves de programmes dans le Calcul des Constructions Inductives}}, - year = {1995} -} - -@Book{Caml, - author = {P. Weis and X. Leroy}, - publisher = {InterEditions}, - title = {Le langage Caml}, - year = {1993} -} - -@InProceedings{ChiPotSimp03, - author = {Laurent Chicli and Lo\"{\i}c Pottier and Carlos Simpson}, - title = {Mathematical Quotients and Quotient Types in Coq}, - booktitle = {TYPES}, - crossref = {DBLP:conf/types/2002}, - year = {2002} -} - -@TechReport{CoC89, - author = {Projet Formel}, - institution = {INRIA}, - number = {110}, - title = {{The Calculus of Constructions. Documentation and user's guide, Version 4.10}}, - year = {1989} -} - -@InProceedings{CoHu85a, - author = {Th. Coquand and G. Huet}, - address = {Linz}, - booktitle = {EUROCAL'85}, - publisher = SV, - series = LNCS, - title = {{Constructions : A Higher Order Proof System for Mechanizing Mathematics}}, - volume = {203}, - year = {1985} -} - -@InProceedings{CoHu85b, - author = {Th. Coquand and G. Huet}, - booktitle = {Logic Colloquium'85}, - editor = {The Paris Logic Group}, - publisher = {North-Holland}, - title = {{Concepts Math\'ematiques et Informatiques formalis\'es dans le Calcul des Constructions}}, - year = {1987} -} - -@Article{CoHu86, - author = {Th. Coquand and G. Huet}, - journal = {Information and Computation}, - number = {2/3}, - title = {The {Calculus of Constructions}}, - volume = {76}, - year = {1988} -} - -@InProceedings{CoPa89, - author = {Th. Coquand and C. Paulin-Mohring}, - booktitle = {Proceedings of Colog'88}, - editor = {P. Martin-L\"of and G. Mints}, - publisher = SV, - series = LNCS, - title = {Inductively defined types}, - volume = {417}, - year = {1990} -} - -@Book{Con86, - author = {R.L. {Constable et al.}}, - publisher = {Prentice-Hall}, - title = {{Implementing Mathematics with the Nuprl Proof Development System}}, - year = {1986} -} - -@PhDThesis{Coq85, - author = {Th. Coquand}, - month = jan, - school = {Universit\'e Paris~7}, - title = {Une Th\'eorie des Constructions}, - year = {1985} -} - -@InProceedings{Coq86, - author = {Th. Coquand}, - address = {Cambridge, MA}, - booktitle = {Symposium on Logic in Computer Science}, - publisher = {IEEE Computer Society Press}, - title = {{An Analysis of Girard's Paradox}}, - year = {1986} -} - -@InProceedings{Coq90, - author = {Th. Coquand}, - booktitle = {Logic and Computer Science}, - editor = {P. Oddifredi}, - note = {INRIA Research Report 1088, also in~\cite{CoC89}}, - publisher = {Academic Press}, - title = {{Metamathematical Investigations of a Calculus of Constructions}}, - year = {1990} -} - -@InProceedings{Coq91, - author = {Th. Coquand}, - booktitle = {Proceedings 9th Int. Congress of Logic, Methodology and Philosophy of Science}, - title = {{A New Paradox in Type Theory}}, - month = {August}, - year = {1991} -} - -@InProceedings{Coq92, - author = {Th. Coquand}, - title = {{Pattern Matching with Dependent Types}}, - year = {1992}, - crossref = {Bastad92} -} - -@InProceedings{Coquand93, - author = {Th. Coquand}, - booktitle = {Types for Proofs and Programs}, - editor = {H. Barendregt and T. Nipokow}, - publisher = SV, - series = LNCS, - title = {{Infinite objects in Type Theory}}, - volume = {806}, - year = {1993}, - pages = {62-78} -} - -@inproceedings{Corbineau08types, - author = {P. Corbineau}, - title = {A Declarative Language for the Coq Proof Assistant}, - editor = {M. Miculan and I. Scagnetto and F. Honsell}, - booktitle = {TYPES '07, Cividale del Friuli, Revised Selected Papers}, - publisher = {Springer}, - series = LNCS, - volume = {4941}, - year = {2007}, - pages = {69-84}, - ee = {http://dx.doi.org/10.1007/978-3-540-68103-8_5}, -} - -@PhDThesis{Cor97, - author = {C. Cornes}, - month = nov, - school = {{Universit\'e Paris 7}}, - title = {Conception d'un langage de haut niveau de représentation de preuves}, - type = {Th\`ese de Doctorat}, - year = {1997} -} - -@MastersThesis{Cou94a, - author = {J. Courant}, - month = sep, - school = {DEA d'Informatique, ENS Lyon}, - title = {Explicitation de preuves par r\'ecurrence implicite}, - year = {1994} -} - -@book{Cur58, - author = {Haskell B. Curry and Robert Feys and William Craig}, - title = {Combinatory Logic}, - volume = 1, - publisher = "North-Holland", - year = 1958, - note = {{\S{9E}}}, -} - -@InProceedings{Del99, - author = {Delahaye, D.}, - title = {Information Retrieval in a Coq Proof Library using - Type Isomorphisms}, - booktitle = {Proceedings of TYPES '99, L\"okeberg}, - publisher = SV, - series = lncs, - year = {1999}, - url = - "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# - "{\sf TYPES99-SIsos.ps.gz}" -} - -@InProceedings{Del00, - author = {Delahaye, D.}, - title = {A {T}actic {L}anguage for the {S}ystem {{\sf Coq}}}, - booktitle = {Proceedings of Logic for Programming and Automated Reasoning - (LPAR), Reunion Island}, - publisher = SV, - series = LNCS, - volume = {1955}, - pages = {85--95}, - month = {November}, - year = {2000}, - url = - "{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# - "{\sf LPAR2000-ltac.ps.gz}" -} - -@InProceedings{DelMay01, - author = {Delahaye, D. and Mayero, M.}, - title = {{\tt Field}: une proc\'edure de d\'ecision pour les nombres r\'eels en {\Coq}}, - booktitle = {Journ\'ees Francophones des Langages Applicatifs, Pontarlier}, - publisher = {INRIA}, - month = {Janvier}, - year = {2001}, - url = - "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# - "{\sf JFLA2000-Field.ps.gz}" -} - -@TechReport{Dow90, - author = {G. Dowek}, - institution = {INRIA}, - number = {1283}, - title = {Naming and Scoping in a Mathematical Vernacular}, - type = {Research Report}, - year = {1990} -} - -@Article{Dow91a, - author = {G. Dowek}, - journal = {Compte-Rendus de l'Acad\'emie des Sciences}, - note = {The undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors}, - number = {12}, - pages = {951--956}, - title = {L'Ind\'ecidabilit\'e du Filtrage du Troisi\`eme Ordre dans les Calculs avec Types D\'ependants ou Constructeurs de Types}, - volume = {I, 312}, - year = {1991} -} - -@InProceedings{Dow91b, - author = {G. Dowek}, - booktitle = {Proceedings of Mathematical Foundation of Computer Science}, - note = {Also INRIA Research Report}, - pages = {151--160}, - publisher = SV, - series = LNCS, - title = {A Second Order Pattern Matching Algorithm in the Cube of Typed $\lambda$-calculi}, - volume = {520}, - year = {1991} -} - -@PhDThesis{Dow91c, - author = {G. Dowek}, - month = dec, - school = {Universit\'e Paris 7}, - title = {D\'emonstration automatique dans le Calcul des Constructions}, - year = {1991} -} - -@Article{Dow92a, - author = {G. Dowek}, - title = {The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable}, - year = 1993, - journal = tcs, - volume = 107, - number = 2, - pages = {349-356} -} - -@Article{Dow94a, - author = {G. Dowek}, - journal = {Annals of Pure and Applied Logic}, - volume = {69}, - pages = {135--155}, - title = {Third order matching is decidable}, - year = {1994} -} - -@InProceedings{Dow94b, - author = {G. Dowek}, - booktitle = {Proceedings of the second international conference on typed lambda calculus and applications}, - title = {Lambda-calculus, Combinators and the Comprehension Schema}, - year = {1995} -} - -@InProceedings{Dyb91, - author = {P. Dybjer}, - booktitle = {Logical Frameworks}, - editor = {G. Huet and G. Plotkin}, - pages = {59--79}, - publisher = {Cambridge University Press}, - title = {Inductive sets and families in {Martin-Löf's} - Type Theory and their set-theoretic semantics: An inversion principle for {Martin-L\"of's} type theory}, - volume = {14}, - year = {1991} -} - -@Article{Dyc92, - author = {Roy Dyckhoff}, - journal = {The Journal of Symbolic Logic}, - month = sep, - number = {3}, - title = {Contraction-free sequent calculi for intuitionistic logic}, - volume = {57}, - year = {1992} -} - -@MastersThesis{Fil94, - author = {J.-C. Filli\^atre}, - month = sep, - school = {DEA d'Informatique, ENS Lyon}, - title = {Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct. Étude et impl\'ementation dans le syst\`eme {\Coq}}, - year = {1994} -} - -@TechReport{Filliatre95, - author = {J.-C. Filli\^atre}, - institution = {LIP-ENS-Lyon}, - title = {A decision procedure for Direct Predicate Calculus}, - type = {Research report}, - number = {96--25}, - year = {1995} -} - -@Article{Filliatre03jfp, - author = {J.-C. Filliâtre}, - title = {Verification of Non-Functional Programs - using Interpretations in Type Theory}, - journal = jfp, - volume = 13, - number = 4, - pages = {709--745}, - month = jul, - year = 2003, - note = {[English translation of \cite{Filliatre99}]}, - url = {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz}, - topics = {team, lri}, - type_publi = {irevcomlec} -} - -@PhDThesis{Filliatre99, - author = {J.-C. Filli\^atre}, - title = {Preuve de programmes imp\'eratifs en th\'eorie des types}, - type = {Thèse de Doctorat}, - school = {Universit\'e Paris-Sud}, - year = 1999, - month = {July}, - url = {\url{http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz}} -} - -@Unpublished{Filliatre99c, - author = {J.-C. Filli\^atre}, - title = {{Formal Proof of a Program: Find}}, - month = {January}, - year = 2000, - note = {Submitted to \emph{Science of Computer Programming}}, - url = {\url{http://www.lri.fr/~filliatr/ftp/publis/find.ps.gz}} -} - -@InProceedings{FilliatreMagaud99, - author = {J.-C. Filli\^atre and N. Magaud}, - title = {Certification of sorting algorithms in the system {\Coq}}, - booktitle = {Theorem Proving in Higher Order Logics: - Emerging Trends}, - year = 1999, - url = {\url{http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz}} -} - -@Unpublished{Fle90, - author = {E. Fleury}, - month = jul, - note = {Rapport de Stage}, - title = {Implantation des algorithmes de {Floyd et de Dijkstra} dans le {Calcul des Constructions}}, - year = {1990} -} - -@Book{Fourier, - author = {Jean-Baptiste-Joseph Fourier}, - publisher = {Gauthier-Villars}, - title = {Fourier's method to solve linear - inequations/equations systems.}, - year = {1890} -} - -@InProceedings{Gim94, - author = {E. Gim\'enez}, - booktitle = {Types'94 : Types for Proofs and Programs}, - note = {Extended version in LIP research report 95-07, ENS Lyon}, - publisher = SV, - series = LNCS, - title = {Codifying guarded definitions with recursive schemes}, - volume = {996}, - year = {1994} -} - -@PhDThesis{Gim96, - author = {E. Gim\'enez}, - title = {Un calcul des constructions infinies et son application \'a la v\'erification de syst\`emes communicants}, - school = {\'Ecole Normale Sup\'erieure de Lyon}, - year = {1996} -} - -@TechReport{Gim98, - author = {E. Gim\'enez}, - title = {A Tutorial on Recursive Types in Coq}, - institution = {INRIA}, - year = 1998, - month = mar -} - -@Unpublished{GimCas05, - author = {E. Gim\'enez and P. Cast\'eran}, - title = {A Tutorial on [Co-]Inductive Types in Coq}, - institution = {INRIA}, - year = 2005, - month = jan, - note = {available at \url{http://coq.inria.fr/doc}} -} - -@InProceedings{Gimenez95b, - author = {E. Gim\'enez}, - booktitle = {Workshop on Types for Proofs and Programs}, - series = LNCS, - number = {1158}, - pages = {135-152}, - title = {An application of co-Inductive types in Coq: - verification of the Alternating Bit Protocol}, - editorS = {S. Berardi and M. Coppo}, - publisher = SV, - year = {1995} -} - -@InProceedings{Gir70, - author = {J.-Y. Girard}, - booktitle = {Proceedings of the 2nd Scandinavian Logic Symposium}, - publisher = {North-Holland}, - title = {Une extension de l'interpr\'etation de {G\"odel} \`a l'analyse, et son application \`a l'\'elimination des coupures dans l'analyse et la th\'eorie des types}, - year = {1970} -} - -@PhDThesis{Gir72, - author = {J.-Y. Girard}, - school = {Universit\'e Paris~7}, - title = {Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur}, - year = {1972} -} - -@Book{Gir89, - author = {J.-Y. Girard and Y. Lafont and P. Taylor}, - publisher = {Cambridge University Press}, - series = {Cambridge Tracts in Theoretical Computer Science 7}, - title = {Proofs and Types}, - year = {1989} -} - -@TechReport{Har95, - author = {John Harrison}, - title = {Metatheory and Reflection in Theorem Proving: A Survey and Critique}, - institution = {SRI International Cambridge Computer Science Research Centre,}, - year = 1995, - type = {Technical Report}, - number = {CRC-053}, - abstract = {http://www.cl.cam.ac.uk/users/jrh/papers.html} -} - -@MastersThesis{Hir94, - author = {D. Hirschkoff}, - month = sep, - school = {DEA IARFA, Ecole des Ponts et Chauss\'ees, Paris}, - title = {Écriture d'une tactique arithm\'etique pour le syst\`eme {\Coq}}, - year = {1994} -} - -@InProceedings{HofStr98, - author = {Martin Hofmann and Thomas Streicher}, - title = {The groupoid interpretation of type theory}, - booktitle = {Proceedings of the meeting Twenty-five years of constructive type theory}, - publisher = {Oxford University Press}, - year = {1998} -} - -@InCollection{How80, - author = {W.A. Howard}, - booktitle = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.}, - editor = {J.P. Seldin and J.R. Hindley}, - note = {Unpublished 1969 Manuscript}, - publisher = {Academic Press}, - title = {The Formulae-as-Types Notion of Constructions}, - year = {1980} -} - -@InProceedings{Hue87tapsoft, - author = {G. Huet}, - title = {Programming of Future Generation Computers}, - booktitle = {Proceedings of TAPSOFT87}, - series = LNCS, - volume = 249, - pages = {276--286}, - year = 1987, - publisher = SV -} - -@InProceedings{Hue87, - author = {G. Huet}, - booktitle = {Programming of Future Generation Computers}, - editor = {K. Fuchi and M. Nivat}, - note = {Also in \cite{Hue87tapsoft}}, - publisher = {Elsevier Science}, - title = {Induction Principles Formalized in the {Calculus of Constructions}}, - year = {1988} -} - -@InProceedings{Hue88, - author = {G. Huet}, - booktitle = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney}, - editor = {R. Narasimhan}, - note = {Also in~\cite{CoC89}}, - publisher = {World Scientific Publishing}, - title = {{The Constructive Engine}}, - year = {1989} -} - -@Unpublished{Hue88b, - author = {G. Huet}, - title = {Extending the Calculus of Constructions with Type:Type}, - year = 1988, - note = {Unpublished} -} - -@Book{Hue89, - editor = {G. Huet}, - publisher = {Addison-Wesley}, - series = {The UT Year of Programming Series}, - title = {Logical Foundations of Functional Programming}, - year = {1989} -} - -@InProceedings{Hue92, - author = {G. Huet}, - booktitle = {Proceedings of 12th FST/TCS Conference, New Delhi}, - pages = {229--240}, - publisher = SV, - series = LNCS, - title = {The Gallina Specification Language : A case study}, - volume = {652}, - year = {1992} -} - -@Article{Hue94, - author = {G. Huet}, - journal = {J. Functional Programming}, - pages = {371--394}, - publisher = {Cambridge University Press}, - title = {Residual theory in $\lambda$-calculus: a formal development}, - volume = {4,3}, - year = {1994} -} - -@InCollection{HuetLevy79, - author = {G. Huet and J.-J. L\'{e}vy}, - title = {Call by Need Computations in Non-Ambigous -Linear Term Rewriting Systems}, - note = {Also research report 359, INRIA, 1979}, - booktitle = {Computational Logic, Essays in Honor of -Alan Robinson}, - editor = {J.-L. Lassez and G. Plotkin}, - publisher = {The MIT press}, - year = {1991} -} - -@Article{KeWe84, - author = {J. Ketonen and R. Weyhrauch}, - journal = {Theoretical Computer Science}, - pages = {297--307}, - title = {A decidable fragment of {P}redicate {C}alculus}, - volume = {32}, - year = {1984} -} - -@Book{Kle52, - author = {S.C. Kleene}, - publisher = {North-Holland}, - series = {Bibliotheca Mathematica}, - title = {Introduction to Metamathematics}, - year = {1952} -} - -@Book{Kri90, - author = {J.-L. Krivine}, - publisher = {Masson}, - series = {Etudes et recherche en informatique}, - title = {Lambda-calcul {types et mod\`eles}}, - year = {1990} -} - -@Book{LE92, - editor = {G. Huet and G. Plotkin}, - publisher = {Cambridge University Press}, - title = {Logical Environments}, - year = {1992} -} - -@Book{LF91, - editor = {G. Huet and G. Plotkin}, - publisher = {Cambridge University Press}, - title = {Logical Frameworks}, - year = {1991} -} - -@Article{Laville91, - author = {A. Laville}, - title = {Comparison of Priority Rules in Pattern -Matching and Term Rewriting}, - journal = {Journal of Symbolic Computation}, - volume = {11}, - pages = {321--347}, - year = {1991} -} - -@InProceedings{LePa94, - author = {F. Leclerc and C. Paulin-Mohring}, - booktitle = {{Types for Proofs and Programs, Types' 93}}, - editor = {H. Barendregt and T. Nipkow}, - publisher = SV, - series = {LNCS}, - title = {{Programming with Streams in Coq. A case study : The Sieve of Eratosthenes}}, - volume = {806}, - year = {1994} -} - -@TechReport{Leroy90, - author = {X. Leroy}, - title = {The {ZINC} experiment: an economical implementation -of the {ML} language}, - institution = {INRIA}, - number = {117}, - year = {1990} -} - -@InProceedings{Let02, - author = {P. Letouzey}, - title = {A New Extraction for Coq}, - booktitle = {TYPES}, - year = 2002, - crossref = {DBLP:conf/types/2002}, - url = {draft at \url{http://www.pps.jussieu.fr/~letouzey/download/extraction2002.ps.gz}} -} - -@PhDThesis{Luo90, - author = {Z. Luo}, - title = {An Extended Calculus of Constructions}, - school = {University of Edinburgh}, - year = {1990} -} - -@inproceedings{Luttik97specificationof, - Author = {Sebastiaan P. Luttik and Eelco Visser}, - Booktitle = {2nd International Workshop on the Theory and Practice of Algebraic Specifications (ASF+SDF'97), Electronic Workshops in Computing}, - Publisher = {Springer-Verlag}, - Title = {Specification of Rewriting Strategies}, - Year = {1997}} - -@Book{MaL84, - author = {{P. Martin-L\"of}}, - publisher = {Bibliopolis}, - series = {Studies in Proof Theory}, - title = {Intuitionistic Type Theory}, - year = {1984} -} - -@Article{MaSi94, - author = {P. Manoury and M. Simonot}, - title = {Automatizing Termination Proofs of Recursively Defined Functions.}, - journal = {TCS}, - volume = {135}, - number = {2}, - year = {1994}, - pages = {319-343}, -} - -@InProceedings{Miquel00, - author = {A. Miquel}, - title = {A Model for Impredicative Type Systems with Universes, -Intersection Types and Subtyping}, - booktitle = {{Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS'00)}}, - publisher = {IEEE Computer Society Press}, - year = {2000} -} - -@PhDThesis{Miquel01a, - author = {A. Miquel}, - title = {Le Calcul des Constructions implicite: syntaxe et s\'emantique}, - month = {dec}, - school = {{Universit\'e Paris 7}}, - year = {2001} -} - -@InProceedings{Miquel01b, - author = {A. Miquel}, - title = {The Implicit Calculus of Constructions: Extending Pure Type Systems with an Intersection Type Binder and Subtyping}, - booktitle = {{Proceedings of the fifth International Conference on Typed Lambda Calculi and Applications (TLCA01), Krakow, Poland}}, - publisher = SV, - series = {LNCS}, - number = 2044, - year = {2001} -} - -@InProceedings{MiWer02, - author = {A. Miquel and B. Werner}, - title = {The Not So Simple Proof-Irrelevant Model of CC}, - booktitle = {TYPES}, - year = {2002}, - pages = {240-258}, - ee = {http://link.springer.de/link/service/series/0558/bibs/2646/26460240.htm}, - crossref = {DBLP:conf/types/2002}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@proceedings{DBLP:conf/types/2002, - editor = {H. Geuvers and F. Wiedijk}, - title = {Types for Proofs and Programs, Second International Workshop, - TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, - Selected Papers}, - booktitle = {TYPES}, - publisher = SV, - series = LNCS, - volume = {2646}, - year = {2003}, - isbn = {3-540-14031-X}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@InProceedings{Moh89a, - author = {C. Paulin-Mohring}, - address = {Austin}, - booktitle = {Sixteenth Annual ACM Symposium on Principles of Programming Languages}, - month = jan, - publisher = {ACM}, - title = {Extracting ${F}_{\omega}$'s programs from proofs in the {Calculus of Constructions}}, - year = {1989} -} - -@PhDThesis{Moh89b, - author = {C. Paulin-Mohring}, - month = jan, - school = {{Universit\'e Paris 7}}, - title = {Extraction de programmes dans le {Calcul des Constructions}}, - year = {1989} -} - -@InProceedings{Moh93, - author = {C. Paulin-Mohring}, - booktitle = {Proceedings of the conference Typed Lambda Calculi and Applications}, - editor = {M. Bezem and J.-F. Groote}, - note = {Also LIP research report 92-49, ENS Lyon}, - number = {664}, - publisher = SV, - series = {LNCS}, - title = {{Inductive Definitions in the System Coq - Rules and Properties}}, - year = {1993} -} - -@Book{Moh97, - author = {C. Paulin-Mohring}, - month = jan, - publisher = {{ENS Lyon}}, - title = {{Le syst\`eme Coq. \mbox{Th\`ese d'habilitation}}}, - year = {1997} -} - -@MastersThesis{Mun94, - author = {C. Muñoz}, - month = sep, - school = {DEA d'Informatique Fondamentale, Universit\'e Paris 7}, - title = {D\'emonstration automatique dans la logique propositionnelle intuitionniste}, - year = {1994} -} - -@PhDThesis{Mun97d, - author = {C. Mu{\~{n}}oz}, - title = {Un calcul de substitutions pour la repr\'esentation - de preuves partielles en th\'eorie de types}, - school = {Universit\'e Paris 7}, - year = {1997}, - note = {Version en anglais disponible comme rapport de - recherche INRIA RR-3309}, - type = {Th\`ese de Doctorat} -} - -@Book{NoPS90, - author = {B. {Nordstr\"om} and K. Peterson and J. Smith}, - booktitle = {Information Processing 83}, - publisher = {Oxford Science Publications}, - series = {International Series of Monographs on Computer Science}, - title = {Programming in {Martin-L\"of's} Type Theory}, - year = {1990} -} - -@Article{Nor88, - author = {B. {Nordstr\"om}}, - journal = {BIT}, - title = {Terminating General Recursion}, - volume = {28}, - year = {1988} -} - -@Book{Odi90, - editor = {P. Odifreddi}, - publisher = {Academic Press}, - title = {Logic and Computer Science}, - year = {1990} -} - -@InProceedings{PaMS92, - author = {M. Parigot and P. Manoury and M. Simonot}, - address = {St. Petersburg, Russia}, - booktitle = {Logic Programming and automated reasoning}, - editor = {A. Voronkov}, - month = jul, - number = {624}, - publisher = SV, - series = {LNCS}, - title = {{ProPre : A Programming language with proofs}}, - year = {1992} -} - -@Article{PaWe92, - author = {C. Paulin-Mohring and B. Werner}, - journal = {Journal of Symbolic Computation}, - pages = {607--640}, - title = {{Synthesis of ML programs in the system Coq}}, - volume = {15}, - year = {1993} -} - -@Article{Par92, - author = {M. Parigot}, - journal = {Theoretical Computer Science}, - number = {2}, - pages = {335--356}, - title = {{Recursive Programming with Proofs}}, - volume = {94}, - year = {1992} -} - -@InProceedings{Parent95b, - author = {C. Parent}, - booktitle = {{Mathematics of Program Construction'95}}, - publisher = SV, - series = {LNCS}, - title = {{Synthesizing proofs from programs in -the Calculus of Inductive Constructions}}, - volume = {947}, - year = {1995} -} - -@InProceedings{Prasad93, - author = {K.V. Prasad}, - booktitle = {{Proceedings of CONCUR'93}}, - publisher = SV, - series = {LNCS}, - title = {{Programming with broadcasts}}, - volume = {715}, - year = {1993} -} - -@Book{RC95, - author = {di~Cosmo, R.}, - title = {Isomorphisms of Types: from $\lambda$-calculus to information - retrieval and language design}, - series = {Progress in Theoretical Computer Science}, - publisher = {Birkhauser}, - year = {1995}, - note = {ISBN-0-8176-3763-X} -} - -@TechReport{Rou92, - author = {J. Rouyer}, - institution = {INRIA}, - month = nov, - number = {1795}, - title = {{Développement de l'Algorithme d'Unification dans le Calcul des Constructions}}, - year = {1992} -} - -@Article{Rushby98, - title = {Subtypes for Specifications: Predicate Subtyping in - {PVS}}, - author = {John Rushby and Sam Owre and N. Shankar}, - journal = {IEEE Transactions on Software Engineering}, - pages = {709--720}, - volume = 24, - number = 9, - month = sep, - year = 1998 -} - -@TechReport{Saibi94, - author = {A. Sa\"{\i}bi}, - institution = {INRIA}, - month = dec, - number = {2345}, - title = {{Axiomatization of a lambda-calculus with explicit-substitutions in the Coq System}}, - year = {1994} -} - - -@MastersThesis{Ter92, - author = {D. Terrasse}, - month = sep, - school = {IARFA}, - title = {{Traduction de TYPOL en COQ. Application \`a Mini ML}}, - year = {1992} -} - -@TechReport{ThBeKa92, - author = {L. Th\'ery and Y. Bertot and G. Kahn}, - institution = {INRIA Sophia}, - month = may, - number = {1684}, - title = {Real theorem provers deserve real user-interfaces}, - type = {Research Report}, - year = {1992} -} - -@Book{TrDa89, - author = {A.S. Troelstra and D. van Dalen}, - publisher = {North-Holland}, - series = {Studies in Logic and the foundations of Mathematics, volumes 121 and 123}, - title = {Constructivism in Mathematics, an introduction}, - year = {1988} -} - -@PhDThesis{Wer94, - author = {B. Werner}, - school = {Universit\'e Paris 7}, - title = {Une th\'eorie des constructions inductives}, - type = {Th\`ese de Doctorat}, - year = {1994} -} - -@PhDThesis{Bar99, - author = {B. Barras}, - school = {Universit\'e Paris 7}, - title = {Auto-validation d'un système de preuves avec familles inductives}, - type = {Th\`ese de Doctorat}, - year = {1999} -} - -@Unpublished{ddr98, - author = {D. de Rauglaudre}, - title = {Camlp4 version 1.07.2}, - year = {1998}, - note = {In Camlp4 distribution} -} - -@Article{dowek93, - author = {G. Dowek}, - title = {{A Complete Proof Synthesis Method for the Cube of Type Systems}}, - journal = {Journal Logic Computation}, - volume = {3}, - number = {3}, - pages = {287--315}, - month = {June}, - year = {1993} -} - -@InProceedings{manoury94, - author = {P. Manoury}, - title = {{A User's Friendly Syntax to Define -Recursive Functions as Typed $\lambda-$Terms}}, - booktitle = {{Types for Proofs and Programs, TYPES'94}}, - series = {LNCS}, - volume = {996}, - month = jun, - year = {1994} -} - -@TechReport{maranget94, - author = {L. Maranget}, - institution = {INRIA}, - number = {2385}, - title = {{Two Techniques for Compiling Lazy Pattern Matching}}, - year = {1994} -} - -@InProceedings{puel-suarez90, - author = {L.Puel and A. Su\'arez}, - booktitle = {{Conference Lisp and Functional Programming}}, - series = {ACM}, - publisher = SV, - title = {{Compiling Pattern Matching by Term -Decomposition}}, - year = {1990} -} - -@MastersThesis{saidi94, - author = {H. Saidi}, - month = sep, - school = {DEA d'Informatique Fondamentale, Universit\'e Paris 7}, - title = {R\'esolution d'\'equations dans le syst\`eme T - de G\"odel}, - year = {1994} -} - -@inproceedings{sozeau06, - author = {Matthieu Sozeau}, - title = {Subset Coercions in {C}oq}, - year = {2007}, - booktitle = {TYPES'06}, - pages = {237-252}, - volume = {4502}, - publisher = "Springer", - series = {LNCS} -} - -@inproceedings{sozeau08, - Author = {Matthieu Sozeau and Nicolas Oury}, - booktitle = {TPHOLs'08}, - Pdf = {http://www.lri.fr/~sozeau/research/publications/drafts/classes.pdf}, - Title = {{F}irst-{C}lass {T}ype {C}lasses}, - Year = {2008}, -} - -@Misc{streicher93semantical, - author = {T. Streicher}, - title = {Semantical Investigations into Intensional Type Theory}, - note = {Habilitationsschrift, LMU Munchen.}, - year = {1993} -} - -@Misc{Pcoq, - author = {Lemme Team}, - title = {Pcoq a graphical user-interface for {Coq}}, - note = {\url{http://www-sop.inria.fr/lemme/pcoq/}} -} - -@Misc{ProofGeneral, - author = {David Aspinall}, - title = {Proof General}, - note = {\url{https://proofgeneral.github.io/}} -} - -@Book{CoqArt, - title = {Interactive Theorem Proving and Program Development. - Coq'Art: The Calculus of Inductive Constructions}, - author = {Yves Bertot and Pierre Castéran}, - publisher = {Springer Verlag}, - series = {Texts in Theoretical Computer Science. An EATCS series}, - year = 2004 -} - -@InCollection{wadler87, - author = {P. Wadler}, - title = {Efficient Compilation of Pattern Matching}, - booktitle = {The Implementation of Functional Programming -Languages}, - editor = {S.L. Peyton Jones}, - publisher = {Prentice-Hall}, - year = {1987} -} - -@inproceedings{DBLP:conf/types/CornesT95, - author = {Cristina Cornes and - Delphine Terrasse}, - title = {Automating Inversion of Inductive Predicates in Coq}, - booktitle = {TYPES}, - year = {1995}, - pages = {85-104}, - crossref = {DBLP:conf/types/1995}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} -@proceedings{DBLP:conf/types/1995, - editor = {Stefano Berardi and - Mario Coppo}, - title = {Types for Proofs and Programs, International Workshop TYPES'95, - Torino, Italy, June 5-8, 1995, Selected Papers}, - booktitle = {TYPES}, - publisher = {Springer}, - series = {Lecture Notes in Computer Science}, - volume = {1158}, - year = {1996}, - isbn = {3-540-61780-9}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@inproceedings{DBLP:conf/types/McBride00, - author = {Conor McBride}, - title = {Elimination with a Motive}, - booktitle = {TYPES}, - year = {2000}, - pages = {197-216}, - ee = {http://link.springer.de/link/service/series/0558/bibs/2277/22770197.htm}, - crossref = {DBLP:conf/types/2000}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@proceedings{DBLP:conf/types/2000, - editor = {Paul Callaghan and - Zhaohui Luo and - James McKinna and - Robert Pollack}, - title = {Types for Proofs and Programs, International Workshop, TYPES - 2000, Durham, UK, December 8-12, 2000, Selected Papers}, - booktitle = {TYPES}, - publisher = {Springer}, - series = {Lecture Notes in Computer Science}, - volume = {2277}, - year = {2002}, - isbn = {3-540-43287-6}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@INPROCEEDINGS{sugar, - author = {Alessandro Giovini and Teo Mora and Gianfranco Niesi and Lorenzo Robbiano and Carlo Traverso}, - title = {"One sugar cube, please" or Selection strategies in the Buchberger algorithm}, - booktitle = { Proceedings of the ISSAC'91, ACM Press}, - year = {1991}, - pages = {5--4}, - publisher = {} -} - -@article{LeeWerner11, - author = {Gyesik Lee and - Benjamin Werner}, - title = {Proof-irrelevant model of {CC} with predicative induction - and judgmental equality}, - journal = {Logical Methods in Computer Science}, - volume = {7}, - number = {4}, - year = {2011}, - ee = {http://dx.doi.org/10.2168/LMCS-7(4:5)2011}, - bibsource = {DBLP, http://dblp.uni-trier.de} -} - -@Comment{cross-references, must be at end} - -@Book{Bastad92, - editor = {B. Nordstr\"om and K. Petersson and G. Plotkin}, - publisher = {Available by ftp at site ftp.inria.fr}, - title = {Proceedings of the 1992 Workshop on Types for Proofs and Programs}, - year = {1992} -} - -@Book{Nijmegen93, - editor = {H. Barendregt and T. Nipkow}, - publisher = SV, - series = LNCS, - title = {Types for Proofs and Programs}, - volume = {806}, - year = {1994} -} - -@article{ TheOmegaPaper, - author = "W. Pugh", - title = "The Omega test: a fast and practical integer programming algorithm for dependence analysis", - journal = "Communication of the ACM", - pages = "102--114", - year = "1992", -} - -@inproceedings{CSwcu, - hal_id = {hal-00816703}, - url = {http://hal.inria.fr/hal-00816703}, - title = {{Canonical Structures for the working Coq user}}, - author = {Mahboubi, Assia and Tassi, Enrico}, - booktitle = {{ITP 2013, 4th Conference on Interactive Theorem Proving}}, - publisher = {Springer}, - pages = {19-34}, - address = {Rennes, France}, - volume = {7998}, - editor = {Sandrine Blazy and Christine Paulin and David Pichardie }, - series = {LNCS }, - doi = {10.1007/978-3-642-39634-2\_5 }, - year = {2013}, -} - -@article{CSlessadhoc, - author = {Gonthier, Georges and Ziliani, Beta and Nanevski, Aleksandar and Dreyer, Derek}, - title = {How to Make Ad Hoc Proof Automation Less Ad Hoc}, - journal = {SIGPLAN Not.}, - issue_date = {September 2011}, - volume = {46}, - number = {9}, - month = sep, - year = {2011}, - issn = {0362-1340}, - pages = {163--175}, - numpages = {13}, - url = {http://doi.acm.org/10.1145/2034574.2034798}, - doi = {10.1145/2034574.2034798}, - acmid = {2034798}, - publisher = {ACM}, - address = {New York, NY, USA}, - keywords = {canonical structures, coq, custom proof automation, hoare type theory, interactive theorem proving, tactics, type classes}, -} - -@inproceedings{CompiledStrongReduction, - author = {Benjamin Gr{\'{e}}goire and - Xavier Leroy}, - editor = {Mitchell Wand and - Simon L. Peyton Jones}, - title = {A compiled implementation of strong reduction}, - booktitle = {Proceedings of the Seventh {ACM} {SIGPLAN} International Conference - on Functional Programming {(ICFP} '02), Pittsburgh, Pennsylvania, - USA, October 4-6, 2002.}, - pages = {235--246}, - publisher = {{ACM}}, - year = {2002}, - url = {http://doi.acm.org/10.1145/581478.581501}, - doi = {10.1145/581478.581501}, - timestamp = {Tue, 11 Jun 2013 13:49:16 +0200}, - biburl = {http://dblp.uni-trier.de/rec/bib/conf/icfp/GregoireL02}, - bibsource = {dblp computer science bibliography, http://dblp.org} -} - -@inproceedings{FullReduction, - author = {Mathieu Boespflug and - Maxime D{\'{e}}n{\`{e}}s and - Benjamin Gr{\'{e}}goire}, - editor = {Jean{-}Pierre Jouannaud and - Zhong Shao}, - title = {Full Reduction at Full Throttle}, - booktitle = {Certified Programs and Proofs - First International Conference, {CPP} - 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings}, - series = {Lecture Notes in Computer Science}, - volume = {7086}, - pages = {362--377}, - publisher = {Springer}, - year = {2011}, - url = {http://dx.doi.org/10.1007/978-3-642-25379-9_26}, - doi = {10.1007/978-3-642-25379-9_26}, - timestamp = {Thu, 17 Nov 2011 13:33:48 +0100}, - biburl = {http://dblp.uni-trier.de/rec/bib/conf/cpp/BoespflugDG11}, - bibsource = {dblp computer science bibliography, http://dblp.org} -} diff --git a/doc/refman/coq-listing.tex b/doc/refman/coq-listing.tex deleted file mode 100644 index c69c3b1b8..000000000 --- a/doc/refman/coq-listing.tex +++ /dev/null @@ -1,152 +0,0 @@ -%======================================================================= -% Listings LaTeX package style for Gallina + SSReflect (Assia Mahboubi 2007) - -\lstdefinelanguage{SSR} { - -% Anything betweeen $ becomes LaTeX math mode -mathescape=true, -% Comments may or not include Latex commands -texcl=false, - - -% Vernacular commands -morekeywords=[1]{ -From, Section, Module, End, Require, Import, Export, Defensive, Function, -Variable, Variables, Parameter, Parameters, Axiom, Hypothesis, Hypotheses, -Notation, Local, Tactic, Reserved, Scope, Open, Close, Bind, Delimit, -Definition, Let, Ltac, Fixpoint, CoFixpoint, Add, Morphism, Relation, -Implicit, Arguments, Set, Unset, Contextual, Strict, Prenex, Implicits, -Inductive, CoInductive, Record, Structure, Canonical, Coercion, -Theorem, Lemma, Corollary, Proposition, Fact, Remark, Example, -Proof, Goal, Save, Qed, Defined, Hint, Resolve, Rewrite, View, -Search, Show, Print, Printing, All, Graph, Projections, inside, -outside, Locate, Maximal}, - -% Gallina -morekeywords=[2]{forall, exists, exists2, fun, fix, cofix, struct, - match, with, end, as, in, return, let, if, is, then, else, - for, of, nosimpl}, - -% Sorts -morekeywords=[3]{Type, Prop}, - -% Various tactics, some are std Coq subsumed by ssr, for the manual purpose -morekeywords=[4]{ - pose, set, move, case, elim, apply, clear, - hnf, intro, intros, generalize, rename, pattern, after, - destruct, induction, using, refine, inversion, injection, - rewrite, congr, unlock, compute, ring, field, - replace, fold, unfold, change, cutrewrite, simpl, - have, gen, generally, suff, wlog, suffices, without, loss, nat_norm, - assert, cut, trivial, revert, bool_congr, nat_congr, abstract, - symmetry, transitivity, auto, split, left, right, autorewrite}, - -% Terminators -morekeywords=[5]{ - by, done, exact, reflexivity, tauto, romega, omega, - assumption, solve, contradiction, discriminate}, - - -% Control -morekeywords=[6]{do, last, first, try, idtac, repeat}, - -% Various symbols -% For the ssr manual we turn off the prettyprint of formulas -% literate= -% {->}{{$\rightarrow\,$}}2 -% {->}{{\tt ->}}3 -% {<-}{{$\leftarrow\,$}}2 -% {<-}{{\tt <-}}2 -% {>->}{{$\mapsto$}}3 -% {<=}{{$\leq$}}1 -% {>=}{{$\geq$}}1 -% {<>}{{$\neq$}}1 -% {/\\}{{$\wedge$}}2 -% {\\/}{{$\vee$}}2 -% {<->}{{$\leftrightarrow\;$}}3 -% {<=>}{{$\Leftrightarrow\;$}}3 -% {:nat}{{$~\in\mathbb{N}$}}3 -% {fforall\ }{{$\forall_f\,$}}1 -% {forall\ }{{$\forall\,$}}1 -% {exists\ }{{$\exists\,$}}1 -% {negb}{{$\neg$}}1 -% {spp}{{:*:\,}}1 -% {~}{{$\sim$}}1 -% {\\in}{{$\in\;$}}1 -% {/\\}{$\land\,$}1 -% {:*:}{{$*$}}2 -% {=>}{{$\,\Rightarrow\ $}}1 -% {=>}{{\tt =>}}2 -% {:=}{{{\tt:=}\,\,}}2 -% {==}{{$\equiv$}\,}2 -% {!=}{{$\neq$}\,}2 -% {^-1}{{$^{-1}$}}1 -% {elt'}{elt'}1 -% {=}{{\tt=}\,\,}2 -% {+}{{\tt+}\,\,}2, -literate= - {isn't }{{{\ttfamily\color{dkgreen} isn't }}}1, - -% Comments delimiters, we do turn this off for the manual -%comment=[s]{(*}{*)}, - -% Spaces are not displayed as a special character -showstringspaces=false, - -% String delimiters -morestring=[b]", -morestring=[d]", - -% Size of tabulations -tabsize=3, - -% Enables ASCII chars 128 to 255 -extendedchars=true, - -% Case sensitivity -sensitive=true, - -% Automatic breaking of long lines -breaklines=true, - -% Default style fors listings -basicstyle=\ttfamily, - -% Position of captions is bottom -captionpos=b, - -% Full flexible columns -columns=[l]fullflexible, - -% Style for (listings') identifiers -identifierstyle={\ttfamily\color{black}}, -% Note : highlighting of Coq identifiers is done through a new -% delimiter definition through an lstset at the begining of the -% document. Don't know how to do better. - -% Style for declaration keywords -keywordstyle=[1]{\ttfamily\color{dkviolet}}, - -% Style for gallina keywords -keywordstyle=[2]{\ttfamily\color{dkgreen}}, - -% Style for sorts keywords -keywordstyle=[3]{\ttfamily\color{lightblue}}, - -% Style for tactics keywords -keywordstyle=[4]{\ttfamily\color{dkblue}}, - -% Style for terminators keywords -keywordstyle=[5]{\ttfamily\color{red}}, - - -%Style for iterators -keywordstyle=[6]{\ttfamily\color{dkpink}}, - -% Style for strings -stringstyle=\ttfamily, - -% Style for comments -commentstyle=\rmfamily, - -} diff --git a/doc/refman/coqide-queries.png b/doc/refman/coqide-queries.png deleted file mode 100644 index 7a46ac4e6..000000000 Binary files a/doc/refman/coqide-queries.png and /dev/null differ diff --git a/doc/refman/coqide.png b/doc/refman/coqide.png deleted file mode 100644 index e300401c9..000000000 Binary files a/doc/refman/coqide.png and /dev/null differ diff --git a/doc/refman/headers.hva b/doc/refman/headers.hva deleted file mode 100644 index 9714a29be..000000000 --- a/doc/refman/headers.hva +++ /dev/null @@ -1,44 +0,0 @@ -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% File headers.hva -% Hevea version of headers.sty -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Commands for indexes -%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\usepackage{index} -\makeindex - - -\newindex{tactic}{tacidx}{tacind}{Tactics Index} -\newindex{command}{comidx}{comind}{Vernacular Commands Index} -\newindex{option}{optidx}{optind}{Vernacular Options Index} -\newindex{error}{erridx}{errind}{Index of Error Messages} -\renewindex{default}{idx}{ind}{Global Index} - -\newcommand{\printrefmanindex}[3]{% -\addcontentsline{toc}{chapter}{#2}% -\printindex[#1]% -\cutname{#3}% -} - -\newcommand{\tacindex}[1]{% -\index{#1@\texttt{#1}}\index[tactic]{#1@\texttt{#1}}} -\newcommand{\comindex}[1]{% -\index{#1@\texttt{#1}}\index[command]{#1@\texttt{#1}}} -\newcommand{\optindex}[1]{% -\index{#1@\texttt{#1}}\index[option]{#1@\texttt{#1}}} -\newcommand{\errindex}[1]{\texttt{#1}\index[error]{#1}} -\newcommand{\errindexbis}[2]{\texttt{#1}\index[error]{#2}} -\newcommand{\ttindex}[1]{\index{#1@\texttt{#1}}} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% For the Addendum table of contents -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\newcommand{\aauthor}[1]{{\LARGE \bf #1} \bigskip} % 3 \bigskip's that were here originally - % may be good for LaTeX but too much for HTML -\newcommand{\atableofcontents}{} -\newcommand{\achapter}[1]{\chapter{#1}} -\newcommand{\asection}{\section} -\newcommand{\asubsection}{\subsection} -\newcommand{\asubsubsection}{\subsubsection} diff --git a/doc/refman/headers.sty b/doc/refman/headers.sty deleted file mode 100644 index fb39f687d..000000000 --- a/doc/refman/headers.sty +++ /dev/null @@ -1,88 +0,0 @@ -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% File headers.sty -% Commands for pretty headers, multiple indexes, and the appendix. -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\usepackage{fancyhdr} - -\setlength{\headheight}{14pt} - -\pagestyle{fancyplain} - -\newcommand{\coqfooter}{\tiny Coq Reference Manual, V\coqversion{}, \today} - -\cfoot{} -\lfoot[{\coqfooter}]{} -\rfoot[]{{\coqfooter}} - -\newcommand{\setheaders}[1]{\rhead[\fancyplain{}{\textbf{#1}}]{\fancyplain{}{\thepage}}\lhead[\fancyplain{}{\thepage}]{\fancyplain{}{\textbf{#1}}}} -\newcommand{\defaultheaders}{\rhead[\fancyplain{}{\leftmark}]{\fancyplain{}{\thepage}}\lhead[\fancyplain{}{\thepage}]{\fancyplain{}{\rightmark}}} - -\renewcommand{\chaptermark}[1]{\markboth{{\bf \thechapter~#1}}{}} -\renewcommand{\sectionmark}[1]{\markright{\thesection~#1}} -\renewcommand{\contentsname}{% -\protect\setheaders{Table of contents}Table of contents} -\renewcommand{\bibname}{\protect\setheaders{Bibliography}% -\protect\RefManCutCommand{BEGINBIBLIO=\thepage}% -\protect\addcontentsline{toc}{chapter}{Bibliography}Bibliography} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Commands for indexes -%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\usepackage{index} -\makeindex - -\newindex{tactic}{tacidx}{tacind}{Tactics Index} -\newindex{command}{comidx}{comind}{Vernacular Commands Index} -\newindex{option}{optidx}{optind}{Vernacular Options Index} -\newindex{error}{erridx}{errind}{Index of Error Messages} -\renewindex{default}{idx}{ind}{Global Index} - -\newcommand{\printrefmanindex}[3]{% -\cleardoublepage% -\phantomsection% -\setheaders{#2}% -\addcontentsline{toc}{chapter}{#2}% -\printindex[#1]% -\cutname{#3}% -} - -\newcommand{\tacindex}[1]{% -\index{#1@\texttt{#1}}\index[tactic]{#1@\texttt{#1}}} -\newcommand{\comindex}[1]{% -\index{#1@\texttt{#1}}\index[command]{#1@\texttt{#1}}} -\newcommand{\optindex}[1]{% -\index{#1@\texttt{#1}}\index[option]{#1@\texttt{#1}}} -\newcommand{\errindex}[1]{\texttt{#1}\index[error]{#1}} -\newcommand{\errindexbis}[2]{\texttt{#1}\index[error]{#2}} -\newcommand{\ttindex}[1]{\index{#1@\texttt{#1}}} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% For the Addendum table of contents -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\newcommand{\aauthor}[1]{{\LARGE \bf #1} \bigskip \bigskip \bigskip} -\newcommand{\atableofcontents}{\section*{Contents}\@starttoc{atoc}} -\newcommand{\achapter}[1]{ - \chapter{#1}\addcontentsline{atoc}{chapter}{#1}} -\newcommand{\asection}[1]{ - \section{#1}\addcontentsline{atoc}{section}{#1}} -\newcommand{\asubsection}[1]{ - \subsection{#1}\addcontentsline{atoc}{subsection}{#1}} -\newcommand{\asubsubsection}[1]{ - \subsubsection{#1}\addcontentsline{atoc}{subsubsection}{#1}} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Reference-Manual.sh is generated to cut the Postscript -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -%\@starttoc{sh} -\newwrite\RefManCut@out% -\immediate\openout\RefManCut@out\jobname.sh -\newcommand{\RefManCutCommand}[1]{% -\immediate\write\RefManCut@out{#1}} -\newcommand{\RefManCutClose}{% -\immediate\closeout\RefManCut@out} - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/index.html b/doc/refman/index.html deleted file mode 100644 index b937350e6..000000000 --- a/doc/refman/index.html +++ /dev/null @@ -1,14 +0,0 @@ - - - - -The Coq Proof Assistant Reference Manual - - - - - - - - - diff --git a/doc/refman/menu.html b/doc/refman/menu.html deleted file mode 100644 index 7312ad344..000000000 --- a/doc/refman/menu.html +++ /dev/null @@ -1,32 +0,0 @@ - - - - -
- - - - - - - - - - - -
Cover page
Table of contents
-Bibliography
-Global Index -
-Tactics Index -
-Vernacular Commands Index -
-Vernacular Options Index -
-Index of Error Messages -
- -
- - -- cgit v1.2.3