--- Begin Message ---
Package: wnpp
Severity: wishlist
Owner: Riley Baird <BM-2cVqnDuYbAU5do2DfJTrN7ZbAJ246S4XiX@bitmessage.ch>
* Package name : coq-highschoolgeometry
Version : 8.4+20150620
Upstream Author : Frédérique Guilhot <Frederique.Guilhot@sophia.inria.fr>
* URL :
http://www.lix.polytechnique.fr/coq/pylons/coq/pylons/contribs/view/HighSchoolGeometry/trunk
* License : LGPL-2.1+
Programming Lang: Coq
Description : coq library for high school geometry proofs/formalisation
Created by Frédérique Guilhot, this library consists of a collection of
"chapters" spanning most of the geometry taught in French high schools.
The first part "2-3 dimensional affine geometry" deals with formalising:
points, vectors, barycenters, oriented lengths
collinearity, coplanarity
parallelism and incidence of straight lines
proofs of Thales and Desargues theorems.
In the second part "3 dimensional affine geometry", we prove theorems about:
relative positions of two straight lines in the space
relative positions of a straight line and a plane
relative positions of two planes
parallelism and incidence properties for several planes and straight lines
The third part "2-3 dimensional euclidean geometry" deals with formalising:
scalar product, orthogonal vectors, and unitary vectors
Euclidean distance and orthogonal projection on a line
proofs of Pythagorean theorem, median theorem
The fourth part "space orthogonality" deals with formalising:
orthogonal line and plan
The fifth part "plane euclidean geometry" deals with formalising:
affine coordinate system, orthogonal coordinate system, affine coordinates
oriented angles
trigonometry
proofs of Pythagorean theorem, median theorem, Al-Kashi and sine theorems
perpendicular bisector, isocel triangle, orthocenter
circle, cocyclicity, tangency (line or circle tangent)
signed area, determinant
equations for straight lines and circles in plane geometry
The sixth part "plane transformations", deals with formalising:
translations, homothety
rotations, reflexions
composition of these transformations.
conservation of tangency for these transformations.
In the seventh part "applications", we prove:
Miquel's theorem, orthocenter theorem, Simson line
circle power and plane inversion
Euler line theorem and nine point circle theorem
The eighth part "complex numbers", deals with formalising:
the field properties of complex numbers
application to geometry of complex numbers
This package is a dependency of geoproof.
--- End Message ---
--- Begin Message ---
Source: coq-highschoolgeometry
Source-Version: 8.4+20150620-1
We believe that the bug you reported is fixed in the latest version of
coq-highschoolgeometry, which is due to be installed in the Debian FTP archive.
A summary of the changes between this version and the previous one is
attached.
Thank you for reporting the bug, which will now be closed. If you
have further comments please address them to 789432@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.
Debian distribution maintenance software
pp.
Riley Baird <BM-2cVqnDuYbAU5do2DfJTrN7ZbAJ246S4XiX@bitmessage.ch> (supplier of updated coq-highschoolgeometry package)
(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmaster@ftp-master.debian.org)
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512
Format: 1.8
Date: Sat, 20 Jun 2015 18:58:01 +1000
Source: coq-highschoolgeometry
Binary: coq-highschoolgeometry
Architecture: source all
Version: 8.4+20150620-1
Distribution: unstable
Urgency: low
Maintainer: Riley Baird <BM-2cVqnDuYbAU5do2DfJTrN7ZbAJ246S4XiX@bitmessage.ch>
Changed-By: Riley Baird <BM-2cVqnDuYbAU5do2DfJTrN7ZbAJ246S4XiX@bitmessage.ch>
Description:
coq-highschoolgeometry - coq library for high school geometry proofs/formalisation
Closes: 789432
Changes:
coq-highschoolgeometry (8.4+20150620-1) unstable; urgency=low
.
* Initial release (Closes: #789432)
Checksums-Sha1:
7fbaf03c4bfd2a1840640180bbb8061c52761deb 1941 coq-highschoolgeometry_8.4+20150620-1.dsc
a34c92e67dba50d216a7357ea09fa33ab9a97c38 137848 coq-highschoolgeometry_8.4+20150620.orig.tar.gz
448931884f7d205c5151d246818b9fb87631655c 2568 coq-highschoolgeometry_8.4+20150620-1.debian.tar.xz
b760fa88261f672e2e70dbf3cb69a70408e5828a 1473844 coq-highschoolgeometry_8.4+20150620-1_all.deb
Checksums-Sha256:
197a0e23eda23b592f536491b1aeb7c21d3dd50943a5bfd3c5ad5223fc647fcd 1941 coq-highschoolgeometry_8.4+20150620-1.dsc
784d8de753a9253b3f8ec50bf7b18e8478b17e78aaf8f3ecaaff808fe9b07081 137848 coq-highschoolgeometry_8.4+20150620.orig.tar.gz
616f17d724914663e0fbfe45202f60c228d82ea622e8a18d041ffbc424b60ff1 2568 coq-highschoolgeometry_8.4+20150620-1.debian.tar.xz
bcb4565eaa5f4a2ec4b1afa1f26987ec1f1192b2311d0aaf1b1b5d05b4824c78 1473844 coq-highschoolgeometry_8.4+20150620-1_all.deb
Files:
0596a74e5d45c11db4a9805f0f60dece 1941 math optional coq-highschoolgeometry_8.4+20150620-1.dsc
0c5089edb40b77bbb1910518d4d5654a 137848 math optional coq-highschoolgeometry_8.4+20150620.orig.tar.gz
dba5779c7da64ee23476b535208d3e82 2568 math optional coq-highschoolgeometry_8.4+20150620-1.debian.tar.xz
942e7669772549565f90687e835e23b8 1473844 math optional coq-highschoolgeometry_8.4+20150620-1_all.deb
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1
iQIcBAEBCgAGBQJVyQY2AAoJEHhT2k1JiBrTYvQP/2mkEz5pDI7e2oi0qBJXBw4B
SEh5LSH97+Rr1qGkVGyYxtqOPgVCaD8SRmkMU8NL5l15NaFd6QMbwRNep/o+suAd
h7/FafqMQUa44p4ih99vfhSqjskxbllO078KcMfZHwBFh6Cyt4bcj0RonoA/J/ZW
l6zcsy5g/e5jjURju1rXEB4M3t2WCYEPBeqbpM699mlyO4h/0J+H6i0ioF5o/HCW
ofSJUmH78SpV6miELLG/U9AekNx1/GJ6+Mrpb1DCMDNqbj35FpYq5+Xj9Nv0QJuI
BKFdEqfmakvpz43yW82MmQ/eXqCJjAjoiCT4sRYlTbdfeIohfibGguHEyyVJVrhg
th+qBdqGlcySPnBJgx1QPcK1Gt+QRpqr33Kfa9FK+A6GqauILFdAAIIsfJFHMLCc
ORNsauRh9cN+DLM54tn0E60KZK4W4QOPOcdu3jK/diUSctK1/TioSRlTrBE/4vG2
sJeSw0eplyjoqvJtwI+Vtyjyx+MvFBZd8bJhQwcTcHuD5n5/oyKWF34BY6mAVGo7
C11iuwRBpNE0Te71tOIUHtcfc07+VUMm31aiNa+00Yn6i/vV01VDzgJ5wvoeNJ5D
KFybuTRR4RE0CyzIwlvK92sZByIFvtBklDZlPcNZmXk6/DNTRtBofjSVGNvvl2fM
kqGPLXyckPcJmMaPAj47
=Rm3B
-----END PGP SIGNATURE-----
--- End Message ---