« Up

euclidean-geometry 8.10.0 1 m 35 s

(2020-08-22 02:22:20 UTC)

Context

# 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
conf-findutils      1           Virtual package relying on findutils
conf-m4             1           Virtual package relying on m4
coq                 8.10.dev    Formal proof management system
num                 0           The Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.05.0      The OCaml compiler (virtual package)
ocaml-base-compiler 4.05.0      Official 4.05.0 release
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.8.1       A library manager for OCaml
# opam file:
opam-version: "2.0"
maintainer: "Hugo.Herbelin@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.10" & < "8.11~"}
]
tags: [
  "keyword: plane geometry"
  "keyword: Euclid"
  "keyword: ruler and compass"
  "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.10.0.tar.gz"
  checksum: "md5=7ae2747aaeb3d7536cca4be7a9854642"
}

Lint

Command
true
Return code
0

Dry install

Dry install with the current Coq version:

Command
opam install -y --show-action coq-euclidean-geometry.8.10.0 coq.8.10.dev
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 2h opam install -y --deps-only coq-euclidean-geometry.8.10.0 coq.8.10.dev
Return code
0
Duration
5 s

Install

Command
opam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y -v coq-euclidean-geometry.8.10.0 coq.8.10.dev
Return code
0
Duration
1 m 35 s

Installation size

Total: 13 M

  • 1019 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/L6_Tactics.vo
  • 628 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/G4_Tactics.vo
  • 517 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/K3_Tactics.vo
  • 467 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/L6_Tactics.glob
  • 462 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/F5_Tactics.vo
  • 461 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/I4_Tactics.vo
  • 435 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/J4_Tactics.vo
  • 431 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/H4_Tactics.vo
  • 357 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C7_Tactics.vo
  • 319 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/G4_Tactics.glob
  • 318 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/D5_Tactics.vo
  • 304 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B7_Tactics.vo
  • 295 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/E4_Tactics.vo
  • 263 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/K3_Tactics.glob
  • 243 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N7_Tactics.vo
  • 237 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/J4_Tactics.glob
  • 234 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/F5_Tactics.glob
  • 219 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/I4_Tactics.glob
  • 218 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/M5_Tactics.vo
  • 215 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C7_Tactics.glob
  • 209 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/H4_Tactics.glob
  • 162 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/D5_Tactics.glob
  • 155 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/L6_Tactics.v
  • 153 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B7_Tactics.glob
  • 145 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/E4_Tactics.glob
  • 124 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/G1_Angles.vo
  • 118 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/M5_Tactics.glob
  • 113 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N7_Tactics.glob
  • 94 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N4_DiscreteThales.vo
  • 94 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/I2_Supplement.vo
  • 91 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/G4_Tactics.v
  • 75 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/G3_ParticularAngle.vo
  • 75 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/K3_Tactics.v
  • 73 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/F5_Tactics.v
  • 69 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/I4_Tactics.v
  • 65 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/J4_Tactics.v
  • 64 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N1_DrawingPerpendicularLines.vo
  • 63 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/H4_Tactics.v
  • 63 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/L4_ParallelogrammAngles.glob
  • 62 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/L3_EquidirectedParallelogramm.vo
  • 60 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/L4_ParallelogrammAngles.vo
  • 60 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C7_Tactics.v
  • 59 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/L2_StrictParallelogramm.vo
  • 56 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/H2_ParticularTriangles.vo
  • 56 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/G1_Angles.glob
  • 53 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/D3_SecondDimension.glob
  • 51 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/E4_Tactics.v
  • 51 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/J1_MidLine.vo
  • 50 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/H1_Triangles.vo
  • 50 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/J3_MidProp.vo
  • 49 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N5_UniqueParallel.vo
  • 49 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/D5_Tactics.v
  • 49 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/L1_Parallelogramm.vo
  • 49 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B7_Tactics.v
  • 47 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/K1_RightAngle.vo
  • 47 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/K2_MidLineandRightAngle.vo
  • 47 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/H3_BuildingTriangle.vo
  • 46 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/I2_Supplement.glob
  • 45 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/G3_ParticularAngle.glob
  • 44 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/I1_SupplementaryAngle.vo
  • 43 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/M2_ParallelLines.vo
  • 43 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N7_Tactics.v
  • 43 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C3_SumDistance.vo
  • 41 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N6_ParallelAndPerpendicularLines.vo
  • 41 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/L2_StrictParallelogramm.glob
  • 41 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B3_EquiOrientedProp.glob
  • 41 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/M4_PerpendicularLines.vo
  • 40 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/L5_nParallelogramm.vo
  • 40 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N2_DrawingParallelLine.vo
  • 39 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/F2_MarkSegment.vo
  • 39 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C5_TriangularInequality.glob
  • 38 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/E2_NotEquidirectedIntersection.vo
  • 38 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/M1_SuperImposedLines.vo
  • 37 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N3_ParallelOpposedLine.vo
  • 37 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/J2_MidPoint.vo
  • 36 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/F1_IntersectionDiameterProp.vo
  • 36 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/M5_Tactics.v
  • 35 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/F3_Graduation.vo
  • 35 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/E3_FourPointsIntersection.vo
  • 34 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C3_SumDistance.glob
  • 34 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N5_UniqueParallel.glob
  • 33 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/I3_OpposedAngles.vo
  • 33 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/K2_MidLineandRightAngle.glob
  • 33 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/M3_SecantLines.vo
  • 31 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/F4_ArchimedianDistance.vo
  • 31 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/H2_ParticularTriangles.glob
  • 31 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/G2_AngleProp.vo
  • 31 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/D4_DistanceLt.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/geom.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/F2_MarkSegment.glob
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/D3_SecondDimension.vo
  • 28 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N1_DrawingPerpendicularLines.glob
  • 27 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/J3_MidProp.glob
  • 27 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/L1_Parallelogramm.glob
  • 27 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B5_BetweenProp.glob
  • 27 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C1_Distance.vo
  • 26 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/L3_EquidirectedParallelogramm.glob
  • 25 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/H1_Triangles.glob
  • 24 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/K1_RightAngle.glob
  • 24 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C5_TriangularInequality.vo
  • 23 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B4_RaysProp.glob
  • 22 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/F1_IntersectionDiameterProp.glob
  • 19 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A3_Metrique.glob
  • 19 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/M4_PerpendicularLines.glob
  • 19 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N4_DiscreteThales.glob
  • 18 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/I1_SupplementaryAngle.glob
  • 18 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C1_Distance.glob
  • 17 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N6_ParallelAndPerpendicularLines.glob
  • 17 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/D2_ExistsClockwise.vo
  • 17 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B3_EquiOrientedProp.vo
  • 16 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/E3_FourPointsIntersection.glob
  • 16 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/M1_SuperImposedLines.glob
  • 16 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B5_BetweenProp.vo
  • 16 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/F3_Graduation.glob
  • 15 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/E2_NotEquidirectedIntersection.glob
  • 14 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/E1_IntersectionLinesProp.vo
  • 14 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B6_EquiDirectedProp.vo
  • 14 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N3_ParallelOpposedLine.glob
  • 13 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/G1_Angles.v
  • 13 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B4_RaysProp.vo
  • 13 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/L5_nParallelogramm.glob
  • 13 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/L4_ParallelogrammAngles.v
  • 13 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N2_DrawingParallelLine.glob
  • 12 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B6_EquiDirectedProp.glob
  • 12 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/M2_ParallelLines.glob
  • 12 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/D3_SecondDimension.v
  • 12 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/I3_OpposedAngles.glob
  • 11 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/D1_IntersectionCirclesProp.vo
  • 11 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C4_DistanceLe.glob
  • 11 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A2_Orientation.glob
  • 11 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A7_Tactics.vo
  • 11 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/D1_IntersectionCirclesProp.glob
  • 11 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/J2_MidPoint.glob
  • 11 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/I2_Supplement.v
  • 11 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/F4_ArchimedianDistance.glob
  • 10 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C6_DistanceTimesN.glob
  • 10 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/H3_BuildingTriangle.glob
  • 10 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/G3_ParticularAngle.v
  • 10 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N1_DrawingPerpendicularLines.v
  • 10 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/D4_DistanceLt.glob
  • 9 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/E1_IntersectionLinesProp.glob
  • 9 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B2_CollinearProp.glob
  • 9 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/G2_AngleProp.glob
  • 9 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C2_CircleAndDistance.vo
  • 9 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/M3_SecantLines.glob
  • 9 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C6_DistanceTimesN.vo
  • 9 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/L2_StrictParallelogramm.v
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A3_Metrique.vo
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/J1_MidLine.glob
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/L3_EquidirectedParallelogramm.v
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C5_TriangularInequality.v
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C4_DistanceLe.vo
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B2_CollinearProp.vo
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A5_Cercle.vo
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N5_UniqueParallel.v
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B3_EquiOrientedProp.v
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/D2_ExistsClockwise.glob
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/H2_ParticularTriangles.v
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C3_SumDistance.v
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/J3_MidProp.v
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A4_Droite.vo
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A2_Orientation.vo
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B1_ClockwiseProp.glob
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/F2_MarkSegment.v
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B5_BetweenProp.v
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N4_DiscreteThales.v
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/K2_MidLineandRightAngle.v
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A7_Tactics.glob
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/K1_RightAngle.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/L1_Parallelogramm.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B1_ClockwiseProp.vo
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B4_RaysProp.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C1_Distance.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/F1_IntersectionDiameterProp.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A5_Cercle.glob
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C2_CircleAndDistance.glob
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/H1_Triangles.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A6_Intersection.vo
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/M4_PerpendicularLines.v
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N6_ParallelAndPerpendicularLines.v
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A6_Intersection.glob
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/I1_SupplementaryAngle.v
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/geom.glob
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/E3_FourPointsIntersection.v
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N2_DrawingParallelLine.v
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/M2_ParallelLines.v
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/F3_Graduation.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A4_Droite.glob
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/E2_NotEquidirectedIntersection.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A7_Tactics.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/M1_SuperImposedLines.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B6_EquiDirectedProp.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/J1_MidLine.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/L5_nParallelogramm.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A1_Plan.vo
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A3_Metrique.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/J2_MidPoint.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/D2_ExistsClockwise.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/N3_ParallelOpposedLine.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C4_DistanceLe.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/H3_BuildingTriangle.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/D1_IntersectionCirclesProp.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C6_DistanceTimesN.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/G2_AngleProp.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/I3_OpposedAngles.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/D4_DistanceLt.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/F4_ArchimedianDistance.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/M3_SecantLines.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A2_Orientation.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B2_CollinearProp.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/geom.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/E1_IntersectionLinesProp.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A5_Cercle.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/B1_ClockwiseProp.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A4_Droite.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A6_Intersection.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/C2_CircleAndDistance.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A1_Plan.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/EuclideanGeometry/A1_Plan.v

Uninstall

Command
opam remove -y coq-euclidean-geometry.8.10.0
Return code
0
Missing removes
none
Wrong removes
none

Sources are on GitHub. © Guillaume Claret.