forked from gentoo/gentoo
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
sci-mathematics/coq: fix metadata indentation
Package-Manager: Portage-3.0.14, Repoman-3.0.2 Signed-off-by: Sam James <[email protected]>
- Loading branch information
1 parent
70c713a
commit 2b0624b
Showing
1 changed file
with
22 additions
and
20 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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> |