# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-num base Num library distributed with the OCaml compiler
base-threads base
base-unix base
camlp5 7.14 Preprocessor-pretty-printer of OCaml
conf-findutils 1 Virtual package relying on findutils
conf-perl 2 Virtual package relying on perl
coq 8.5.1 Formal proof management system
num 0 The Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.03.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.03.0 Official 4.03.0 release
ocaml-config 1 OCaml Switch Configuration
# opam file:
opam-version: "2.0"
maintainer: "matej.kosik@inria.fr"
homepage: "https://github.com/coq-contribs/euclidean-geometry"
license: "LGPL"
build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-R" "%{lib}%/coq/user-contrib/EuclideanGeometry"]
depends: [
"ocaml"
"coq" {>= "8.5" & < "8.6~"}
]
tags: [ "keyword:plane geometry" "keyword:euclid" "keyword:ruler and compass geometry" "category:Mathematics/Geometry/General" ]
authors: [ "Jean Duprat <Jean.Duprat@ens-lyon.fr>" ]
bug-reports: "https://github.com/coq-contribs/euclidean-geometry/issues"
dev-repo: "git+https://github.com/coq-contribs/euclidean-geometry.git"
synopsis: "Basis of the Euclid's plane geometry"
description: """
This is a more recent version of the basis of Euclid's plane geometry, the previous version was the contribution intitled RulerCompassGeometry.
The plane geometry is defined as a set of points, with two predicates : Clokwise for the orientation and Equidistant for the metric and three constructors, Ruler for the lines, Compass for the circles and Intersection for the points.
For using it, we suggest to compile the files the name of which begin by a capital letter and a number from A1 to N7 in the lexicographic order and to keep modifiable the files of tacics (from Tactic1 to Tactic4) and the files of examples (Hilbert and Bolyai)."""
flags: light-uninstall
url {
src:
"https://github.com/coq-contribs/euclidean-geometry/archive/v8.5.0.tar.gz"
checksum: "md5=bfd0c53f61b8a85beaa0a347ee7971a7"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-euclidean-geometry.8.5.0 coq.8.5.1Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-euclidean-geometry.8.5.0 coq.8.5.1opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-euclidean-geometry.8.5.0 coq.8.5.1Total: 11 M
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L6_Tactics.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L6_Tactics.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G4_Tactics.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/K3_Tactics.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I4_Tactics.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F5_Tactics.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G4_Tactics.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J4_Tactics.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H4_Tactics.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/K3_Tactics.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C7_Tactics.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D5_Tactics.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J4_Tactics.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F5_Tactics.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B7_Tactics.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I4_Tactics.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E4_Tactics.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C7_Tactics.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H4_Tactics.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N7_Tactics.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M5_Tactics.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D5_Tactics.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L6_Tactics.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B7_Tactics.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E4_Tactics.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G1_Angles.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M5_Tactics.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N7_Tactics.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I2_Supplement.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N4_DiscreteThales.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G4_Tactics.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G3_ParticularAngle.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/K3_Tactics.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F5_Tactics.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N1_DrawingPerpendicularLines.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I4_Tactics.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J4_Tactics.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L3_EquidirectedParallelogramm.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L4_ParallelogrammAngles.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H4_Tactics.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L4_ParallelogrammAngles.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L2_StrictParallelogramm.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C7_Tactics.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H2_ParticularTriangles.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G1_Angles.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D3_SecondDimension.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H1_Triangles.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J3_MidProp.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N5_UniqueParallel.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J1_MidLine.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L1_Parallelogramm.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E4_Tactics.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/K1_RightAngle.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/K2_MidLineandRightAngle.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D5_Tactics.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H3_BuildingTriangle.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B7_Tactics.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I1_SupplementaryAngle.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I2_Supplement.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G3_ParticularAngle.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M2_ParallelLines.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N6_ParallelAndPerpendicularLines.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N7_Tactics.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M4_PerpendicularLines.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C3_SumDistance.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N2_DrawingParallelLine.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L5_nParallelogramm.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F2_MarkSegment.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B3_EquiOrientedProp.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E2_NotEquidirectedIntersection.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L2_StrictParallelogramm.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M1_SuperImposedLines.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N3_ParallelOpposedLine.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J2_MidPoint.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C5_TriangularInequality.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F1_IntersectionDiameterProp.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F3_Graduation.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E3_FourPointsIntersection.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M5_Tactics.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I3_OpposedAngles.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M3_SecantLines.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C3_SumDistance.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N5_UniqueParallel.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/K2_MidLineandRightAngle.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F4_ArchimedianDistance.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D4_DistanceLt.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G2_AngleProp.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/geom.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D3_SecondDimension.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H2_ParticularTriangles.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F2_MarkSegment.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N1_DrawingPerpendicularLines.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J3_MidProp.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B5_BetweenProp.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C1_Distance.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L3_EquidirectedParallelogramm.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L1_Parallelogramm.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H1_Triangles.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C5_TriangularInequality.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/K1_RightAngle.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B4_RaysProp.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F1_IntersectionDiameterProp.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N4_DiscreteThales.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I1_SupplementaryAngle.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M4_PerpendicularLines.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A3_Metrique.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C1_Distance.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B3_EquiOrientedProp.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N6_ParallelAndPerpendicularLines.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D2_ExistsClockwise.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B5_BetweenProp.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E3_FourPointsIntersection.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M1_SuperImposedLines.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F3_Graduation.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E2_NotEquidirectedIntersection.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B4_RaysProp.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B6_EquiDirectedProp.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E1_IntersectionLinesProp.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N3_ParallelOpposedLine.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L5_nParallelogramm.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G1_Angles.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L4_ParallelogrammAngles.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N2_DrawingParallelLine.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B6_EquiDirectedProp.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M2_ParallelLines.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D1_IntersectionCirclesProp.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D3_SecondDimension.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C4_DistanceLe.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A2_Orientation.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J2_MidPoint.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D1_IntersectionCirclesProp.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I2_Supplement.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I3_OpposedAngles.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F4_ArchimedianDistance.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C6_DistanceTimesN.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H3_BuildingTriangle.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G3_ParticularAngle.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A7_Tactics.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N1_DrawingPerpendicularLines.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D4_DistanceLt.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E1_IntersectionLinesProp.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B2_CollinearProp.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G2_AngleProp.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C2_CircleAndDistance.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C6_DistanceTimesN.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A3_Metrique.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M3_SecantLines.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L2_StrictParallelogramm.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J1_MidLine.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L3_EquidirectedParallelogramm.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B2_CollinearProp.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C4_DistanceLe.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A5_Cercle.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C5_TriangularInequality.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N5_UniqueParallel.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A2_Orientation.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B3_EquiOrientedProp.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D2_ExistsClockwise.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A4_Droite.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H2_ParticularTriangles.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C3_SumDistance.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J3_MidProp.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B1_ClockwiseProp.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F2_MarkSegment.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B5_BetweenProp.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N4_DiscreteThales.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/K2_MidLineandRightAngle.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A7_Tactics.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/K1_RightAngle.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B1_ClockwiseProp.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L1_Parallelogramm.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B4_RaysProp.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C1_Distance.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F1_IntersectionDiameterProp.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A6_Intersection.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A5_Cercle.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H1_Triangles.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C2_CircleAndDistance.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M4_PerpendicularLines.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N6_ParallelAndPerpendicularLines.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I1_SupplementaryAngle.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A6_Intersection.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/geom.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E3_FourPointsIntersection.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M2_ParallelLines.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N2_DrawingParallelLine.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F3_Graduation.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E2_NotEquidirectedIntersection.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A4_Droite.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A7_Tactics.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M1_SuperImposedLines.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B6_EquiDirectedProp.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A1_Plan.vo../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J1_MidLine.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L5_nParallelogramm.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A3_Metrique.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J2_MidPoint.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N3_ParallelOpposedLine.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C4_DistanceLe.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D2_ExistsClockwise.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H3_BuildingTriangle.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D1_IntersectionCirclesProp.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C6_DistanceTimesN.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G2_AngleProp.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I3_OpposedAngles.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D4_DistanceLt.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F4_ArchimedianDistance.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M3_SecantLines.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A2_Orientation.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B2_CollinearProp.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/geom.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E1_IntersectionLinesProp.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A5_Cercle.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B1_ClockwiseProp.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A4_Droite.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A6_Intersection.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C2_CircleAndDistance.v../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A1_Plan.glob../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A1_Plan.vopam remove -y coq-euclidean-geometry.8.5.0