commit: 2b0624b89cf627b5dc96bee1c7e33f90ae3f733d Author: Sam James <sam <AT> gentoo <DOT> org> AuthorDate: Mon Feb 8 07:36:55 2021 +0000 Commit: Sam James <sam <AT> gentoo <DOT> org> CommitDate: Mon Feb 8 07:36:55 2021 +0000 URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=2b0624b8
sci-mathematics/coq: fix metadata indentation Package-Manager: Portage-3.0.14, Repoman-3.0.2 Signed-off-by: Sam James <sam <AT> gentoo.org> sci-mathematics/coq/metadata.xml | 42 +++++++++++++++++++++------------------- 1 file changed, 22 insertions(+), 20 deletions(-) diff --git a/sci-mathematics/coq/metadata.xml b/sci-mathematics/coq/metadata.xml index 3dd30ec8636..f49ad93c8b0 100644 --- a/sci-mathematics/coq/metadata.xml +++ b/sci-mathematics/coq/metadata.xml @@ -1,24 +1,26 @@ <?xml version="1.0" encoding="UTF-8"?> <!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd";> <pkgmetadata> - <maintainer type="project"> - <email>[email protected]</email> - <name>Gentoo Mathematics Project</name> - </maintainer> - <longdescription lang="en"> - Developed in the LogiCal project, the Coq tool is a formal proof - management system: a proof done with Coq is mechanically checked - by the machine. - In particular, Coq allows: - * the definition of functions or predicates, - * to state mathematical theorems and software specifications, - * to develop interactively formal proofs of these theorems, - * to check these proofs by a small certification "kernel". - Coq is based on a logical framework called "Calculus of Inductive - Constructions" extended by a modular development system for - theories. -</longdescription> - <use> - <flag name="camlp5">Build using camlp5. This is required for some plugins like Ssreflect.</flag> - </use> + <maintainer type="project"> + <email>[email protected]</email> + <name>Gentoo Mathematics Project</name> + </maintainer> + <longdescription lang="en"> + Developed in the LogiCal project, the Coq tool is a formal proof + management system: a proof done with Coq is mechanically checked + by the machine. + + In particular, Coq allows: + * the definition of functions or predicates, + * to state mathematical theorems and software specifications, + * to develop interactively formal proofs of these theorems, + * to check these proofs by a small certification "kernel". + + Coq is based on a logical framework called "Calculus of Inductive + Constructions" extended by a modular development system for + theories. + </longdescription> + <use> + <flag name="camlp5">Build using camlp5. This is required for some plugins like Ssreflect.</flag> + </use> </pkgmetadata>
