[Pkg-ocaml-maint-commits] [SCM] coq-doc packaging branch, master, updated. debian/8.1-3-27-gabb5c8e

[Stephane Glondu]

The following commit has been merged in the master branch:
commit 3cc3ec9b6f6ac3a6852ac39ef00c3e1c68df576e
Author: Stephane Glondu <steph at glondu.net>
Date:   Thu Jan 7 15:55:10 2010 +0100

    Register PDF in doc-base, too

diff --git a/debian/coq-doc-html.doc-base.faq b/debian/coq-doc-html.doc-base.faq
index 57bfc7c..79e34ad 100644
--- a/debian/coq-doc-html.doc-base.faq
+++ b/debian/coq-doc-html.doc-base.faq
@@ -1,4 +1,4 @@
-Document: coq-faq
+Document: coq-faq-html
 Title: Coq Version 8.0 for the Clueless (FAQ)
 Author: Hugo Herbelin, Florent Kirchner, Benjamin Monate, Julien Narboux
 Abstract: This note intends to provide an easy way to get acquainted with the Coq theorem prover. It tries to formulate appropriate answers to some of the questions any newcomers will face, and to give pointers to other references when possible.
diff --git a/debian/coq-doc-html.doc-base.manual b/debian/coq-doc-html.doc-base.manual
index 08d7135..cf7b9a2 100644
--- a/debian/coq-doc-html.doc-base.manual
+++ b/debian/coq-doc-html.doc-base.manual
@@ -1,4 +1,4 @@
-Document: coq-manual
+Document: coq-manual-html
 Title: The Coq Proof Assistant Reference Manual
 Author: The Coq Development Team
 Abstract: Reference Manual of version 8.0 of the Coq proof assistant which is a system designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that programs are correct with respect to their specification.
diff --git a/debian/coq-doc-html.doc-base.rectutorial b/debian/coq-doc-html.doc-base.rectutorial
index 9390255..8bd3046 100644
--- a/debian/coq-doc-html.doc-base.rectutorial
+++ b/debian/coq-doc-html.doc-base.rectutorial
@@ -1,4 +1,4 @@
-Document: coq-rectutorial
+Document: coq-rectutorial-html
 Title: The Coq Proof Assistant -- A Tutorial on [Co-]Inductive types in Coq
 Author: Eduardo Giménez and Pierre Castéran
 Abstract: This document is an introduction to the definition and use of inductive and co-inductive types in the Coq proof environment. It explains how types like natural numbers and infinite streams are defined in Coq, and the kind of proof techniques that can be used to reason about them (case analysis, induction, inversion of predicates, co-induction, etc). Each technique is illustrated through an executable and self-contained Coq script.
diff --git a/debian/coq-doc-html.doc-base.tutorial b/debian/coq-doc-html.doc-base.tutorial
index 063dcea..406f2e2 100644
--- a/debian/coq-doc-html.doc-base.tutorial
+++ b/debian/coq-doc-html.doc-base.tutorial
@@ -1,4 +1,4 @@
-Document: coq-tutorial
+Document: coq-tutorial-html
 Title: The Coq Proof Assistant -- A Tutorial
 Author: Gérard Huet, Gilles Kahn and Christine Paulin-Mohring
 Abstract: This documents presents in the most elementary manner a tutorial on the basic specification language of the Coq proof-assistant, called Gallina, in which formal axiomatisations may be developed, and on the main proof tools.
diff --git a/debian/coq-doc-html.doc-base.faq b/debian/coq-doc-pdf.doc-base.faq
similarity index 76%
copy from debian/coq-doc-html.doc-base.faq
copy to debian/coq-doc-pdf.doc-base.faq
index 57bfc7c..c09f1dd 100644
--- a/debian/coq-doc-html.doc-base.faq
+++ b/debian/coq-doc-pdf.doc-base.faq
@@ -1,9 +1,8 @@
-Document: coq-faq
+Document: coq-faq-pdf
 Title: Coq Version 8.0 for the Clueless (FAQ)
 Author: Hugo Herbelin, Florent Kirchner, Benjamin Monate, Julien Narboux
 Abstract: This note intends to provide an easy way to get acquainted with the Coq theorem prover. It tries to formulate appropriate answers to some of the questions any newcomers will face, and to give pointers to other references when possible.
 Section: Science/Mathematics
 
-Format: HTML
-Index: /usr/share/doc/coq-doc-html/FAQ.v.html
-Files: /usr/share/doc/coq-doc-html/FAQ.v.html
+Format: PDF
+Files: /usr/share/doc/coq-doc-pdf/FAQ.v.pdf*
diff --git a/debian/coq-doc-html.doc-base.manual b/debian/coq-doc-pdf.doc-base.manual
similarity index 73%
copy from debian/coq-doc-html.doc-base.manual
copy to debian/coq-doc-pdf.doc-base.manual
index 08d7135..3b8a8a4 100644
--- a/debian/coq-doc-html.doc-base.manual
+++ b/debian/coq-doc-pdf.doc-base.manual
@@ -1,9 +1,8 @@
-Document: coq-manual
+Document: coq-manual-pdf
 Title: The Coq Proof Assistant Reference Manual
 Author: The Coq Development Team
 Abstract: Reference Manual of version 8.0 of the Coq proof assistant which is a system designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that programs are correct with respect to their specification.
 Section: Science/Mathematics
 
-Format: HTML
-Index: /usr/share/doc/coq-doc-html/refman/index.html
-Files: /usr/share/doc/coq-doc-html/refman/*.html
+Format: PDF
+Files: /usr/share/doc/coq-doc-pdf/Reference-Manual.pdf*
diff --git a/debian/coq-doc-html.doc-base.rectutorial b/debian/coq-doc-pdf.doc-base.rectutorial
similarity index 80%
copy from debian/coq-doc-html.doc-base.rectutorial
copy to debian/coq-doc-pdf.doc-base.rectutorial
index 9390255..de5ef82 100644
--- a/debian/coq-doc-html.doc-base.rectutorial
+++ b/debian/coq-doc-pdf.doc-base.rectutorial
@@ -1,9 +1,8 @@
-Document: coq-rectutorial
+Document: coq-rectutorial-pdf
 Title: The Coq Proof Assistant -- A Tutorial on [Co-]Inductive types in Coq
 Author: Eduardo Giménez and Pierre Castéran
 Abstract: This document is an introduction to the definition and use of inductive and co-inductive types in the Coq proof environment. It explains how types like natural numbers and infinite streams are defined in Coq, and the kind of proof techniques that can be used to reason about them (case analysis, induction, inversion of predicates, co-induction, etc). Each technique is illustrated through an executable and self-contained Coq script.
 Section: Science/Mathematics
 
-Format: HTML
-Index: /usr/share/doc/coq-doc-html/RecTutorial.html
-Files: /usr/share/doc/coq-doc-html/RecTutorial.html
+Format: PDF
+Files: /usr/share/doc/coq-doc-pdf/RecTutorial.pdf*
diff --git a/debian/coq-doc-html.doc-base.tutorial b/debian/coq-doc-pdf.doc-base.tutorial
similarity index 72%
copy from debian/coq-doc-html.doc-base.tutorial
copy to debian/coq-doc-pdf.doc-base.tutorial
index 063dcea..55f3a20 100644
--- a/debian/coq-doc-html.doc-base.tutorial
+++ b/debian/coq-doc-pdf.doc-base.tutorial
@@ -1,9 +1,8 @@
-Document: coq-tutorial
+Document: coq-tutorial-pdf
 Title: The Coq Proof Assistant -- A Tutorial
 Author: Gérard Huet, Gilles Kahn and Christine Paulin-Mohring
 Abstract: This documents presents in the most elementary manner a tutorial on the basic specification language of the Coq proof-assistant, called Gallina, in which formal axiomatisations may be developed, and on the main proof tools.
 Section: Science/Mathematics
 
-Format: HTML
-Index: /usr/share/doc/coq-doc-html/Tutorial.v.html
-Files: /usr/share/doc/coq-doc-html/Tutorial.v.html
+Format: PDF
+Files: /usr/share/doc/coq-doc-pdf/Tutorial.v.pdf*

-- 
coq-doc packaging