[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 3441e6289d9b74945dda648f29939b4b77024503
Author: Stephane Glondu <steph at glondu.net>
Date:   Thu Jan 7 15:45:02 2010 +0100

    Various fixes thanks to Lintian

diff --git a/debian/control b/debian/control
index 72fc710..fb5729b 100644
--- a/debian/control
+++ b/debian/control
@@ -22,31 +22,33 @@ Vcs-Browser: http://git.debian.org/?p=pkg-ocaml-maint/packages/coq-doc.git
 
 Package: coq-doc
 Architecture: all
-Depends: coq-doc-html, coq-doc-pdf
-Description: documentation for Coq in html format
+Depends: coq-doc-html, coq-doc-pdf, ${misc:Depends}
+Description: documentation for Coq
  Coq is a proof assistant for higher-order logic, which allows the
  development of computer programs consistent with their formal
- specification. It is developed using Objective Caml and Camlp4.
+ specification. It is developed using Objective Caml and Camlp5.
  .
  This is a dummy package which will install the documentation in html and
  pdf formats.
 
 Package: coq-doc-html
 Architecture: all
+Depends: ${misc:Depends}
 Replaces: coq-doc (<= 8.0pl1.0-1)
 Description: documentation for Coq in html format
  Coq is a proof assistant for higher-order logic, which allows the
  development of computer programs consistent with their formal
- specification. It is developed using Objective Caml and Camlp4.
+ specification. It is developed using Objective Caml and Camlp5.
  .
  This package contains its documentation and tutorials in html format.
 
 Package: coq-doc-pdf
 Architecture: all
+Depends: ${misc:Depends}
 Replaces: coq-doc (<= 8.0pl1.0-1)
 Description: documentation for Coq in pdf format
  Coq is a proof assistant for higher-order logic, which allows the
  development of computer programs consistent with their formal
- specification. It is developed using Objective Caml and Camlp4.
+ specification. It is developed using Objective Caml and Camlp5.
  .
  This package contains its documentation and tutorials in pdf format.
diff --git a/debian/coq-doc-html.doc-base.faq b/debian/coq-doc-html.doc-base.faq
index 032e13e..57bfc7c 100644
--- a/debian/coq-doc-html.doc-base.faq
+++ b/debian/coq-doc-html.doc-base.faq
@@ -2,7 +2,7 @@ Document: coq-faq
 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: Apps/Math
+Section: Science/Mathematics
 
 Format: HTML
 Index: /usr/share/doc/coq-doc-html/FAQ.v.html
diff --git a/debian/coq-doc-html.doc-base.manual b/debian/coq-doc-html.doc-base.manual
index de21981..08d7135 100644
--- a/debian/coq-doc-html.doc-base.manual
+++ b/debian/coq-doc-html.doc-base.manual
@@ -2,7 +2,7 @@ Document: coq-manual
 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: Apps/Math
+Section: Science/Mathematics
 
 Format: HTML
 Index: /usr/share/doc/coq-doc-html/refman/index.html
diff --git a/debian/coq-doc-html.doc-base.rectutorial b/debian/coq-doc-html.doc-base.rectutorial
index 7021ae1..9390255 100644
--- a/debian/coq-doc-html.doc-base.rectutorial
+++ b/debian/coq-doc-html.doc-base.rectutorial
@@ -1,9 +1,9 @@
 Document: coq-rectutorial
 Title: The Coq Proof Assistant -- A Tutorial on [Co-]Inductive types in Coq
-Author: Eduardo Giménez and Pierre Castéran
+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: Apps/Math
+Section: Science/Mathematics
 
 Format: HTML
-Index: /usr/share/doc/coq-doc-html/RecTutorial.v.html
-Files: /usr/share/doc/coq-doc-html/RecTutorial.v.html
+Index: /usr/share/doc/coq-doc-html/RecTutorial.html
+Files: /usr/share/doc/coq-doc-html/RecTutorial.html
diff --git a/debian/coq-doc-html.doc-base.tutorial b/debian/coq-doc-html.doc-base.tutorial
index 96c39e7..063dcea 100644
--- a/debian/coq-doc-html.doc-base.tutorial
+++ b/debian/coq-doc-html.doc-base.tutorial
@@ -2,7 +2,7 @@ Document: coq-tutorial
 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: Apps/Math
+Section: Science/Mathematics
 
 Format: HTML
 Index: /usr/share/doc/coq-doc-html/Tutorial.v.html

-- 
coq-doc packaging