summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSam James <sam@gentoo.org>2021-02-08 07:36:55 +0000
committerSam James <sam@gentoo.org>2021-02-08 07:36:55 +0000
commit2b0624b89cf627b5dc96bee1c7e33f90ae3f733d (patch)
tree26d512ee0237efb302c314bd632311656721e493 /sci-mathematics/coq
parentsci-mathematics/coq: lower OCaml dep (diff)
downloadgentoo-2b0624b89cf627b5dc96bee1c7e33f90ae3f733d.tar.gz
gentoo-2b0624b89cf627b5dc96bee1c7e33f90ae3f733d.tar.bz2
gentoo-2b0624b89cf627b5dc96bee1c7e33f90ae3f733d.zip
sci-mathematics/coq: fix metadata indentation
Package-Manager: Portage-3.0.14, Repoman-3.0.2 Signed-off-by: Sam James <sam@gentoo.org>
Diffstat (limited to 'sci-mathematics/coq')
-rw-r--r--sci-mathematics/coq/metadata.xml42
1 files changed, 22 insertions, 20 deletions
diff --git a/sci-mathematics/coq/metadata.xml b/sci-mathematics/coq/metadata.xml
index 3dd30ec86367..f49ad93c8b0c 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>sci-mathematics@gentoo.org</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>sci-mathematics@gentoo.org</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>