ยซ Up

euclidean-geometry 8.7.0 2 m 0 s ๐Ÿ†

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
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.7.1+2     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
ocamlfind           1.9.6       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.7" & < "8.8~"}
]
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.7.0.tar.gz"
  checksum: "md5=64bd0e87e9d61dfc9de79aeb1d91875f"
}

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.7.0 coq.8.7.1+2
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 4h opam install -y --deps-only coq-euclidean-geometry.8.7.0 coq.8.7.1+2
Return code
0
Duration
1 m 0 s

Install ๐Ÿš€

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-euclidean-geometry.8.7.0 coq.8.7.1+2
Return code
0
Duration
2 m 0 s

Installation size

Total: 13 M

  • 1 M ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L6_Tactics.vo
  • 627 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G4_Tactics.vo
  • 523 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/K3_Tactics.vo
  • 466 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I4_Tactics.vo
  • 466 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L6_Tactics.glob
  • 458 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F5_Tactics.vo
  • 437 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H4_Tactics.vo
  • 437 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J4_Tactics.vo
  • 353 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C7_Tactics.vo
  • 321 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D5_Tactics.vo
  • 318 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G4_Tactics.glob
  • 303 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B7_Tactics.vo
  • 295 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E4_Tactics.vo
  • 262 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/K3_Tactics.glob
  • 247 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N7_Tactics.vo
  • 236 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J4_Tactics.glob
  • 234 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F5_Tactics.glob
  • 226 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M5_Tactics.vo
  • 218 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I4_Tactics.glob
  • 215 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C7_Tactics.glob
  • 209 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H4_Tactics.glob
  • 162 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D5_Tactics.glob
  • 155 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L6_Tactics.v
  • 153 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B7_Tactics.glob
  • 145 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E4_Tactics.glob
  • 128 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G1_Angles.vo
  • 118 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M5_Tactics.glob
  • 112 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N7_Tactics.glob
  • 96 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I2_Supplement.vo
  • 95 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N4_DiscreteThales.vo
  • 91 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G4_Tactics.v
  • 78 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G3_ParticularAngle.vo
  • 75 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/K3_Tactics.v
  • 73 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F5_Tactics.v
  • 69 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I4_Tactics.v
  • 67 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N1_DrawingPerpendicularLines.vo
  • 65 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J4_Tactics.v
  • 64 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L3_EquidirectedParallelogramm.vo
  • 63 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L4_ParallelogrammAngles.vo
  • 63 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H4_Tactics.v
  • 63 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L4_ParallelogrammAngles.glob
  • 62 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L2_StrictParallelogramm.vo
  • 60 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C7_Tactics.v
  • 59 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H2_ParticularTriangles.vo
  • 56 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G1_Angles.glob
  • 53 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D3_SecondDimension.glob
  • 53 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H1_Triangles.vo
  • 52 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J3_MidProp.vo
  • 52 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N5_UniqueParallel.vo
  • 51 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J1_MidLine.vo
  • 51 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L1_Parallelogramm.vo
  • 51 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E4_Tactics.v
  • 50 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/K1_RightAngle.vo
  • 50 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/K2_MidLineandRightAngle.vo
  • 49 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D5_Tactics.v
  • 49 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H3_BuildingTriangle.vo
  • 49 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B7_Tactics.v
  • 46 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I2_Supplement.glob
  • 46 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I1_SupplementaryAngle.vo
  • 45 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M2_ParallelLines.vo
  • 45 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G3_ParticularAngle.glob
  • 44 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N6_ParallelAndPerpendicularLines.vo
  • 43 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M4_PerpendicularLines.vo
  • 43 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N7_Tactics.v
  • 43 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C3_SumDistance.vo
  • 42 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L5_nParallelogramm.vo
  • 42 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N2_DrawingParallelLine.vo
  • 42 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F2_MarkSegment.vo
  • 41 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B3_EquiOrientedProp.glob
  • 40 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L2_StrictParallelogramm.glob
  • 40 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E2_NotEquidirectedIntersection.vo
  • 40 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M1_SuperImposedLines.vo
  • 39 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N3_ParallelOpposedLine.vo
  • 39 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J2_MidPoint.vo
  • 38 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C5_TriangularInequality.glob
  • 38 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F1_IntersectionDiameterProp.vo
  • 37 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F3_Graduation.vo
  • 37 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E3_FourPointsIntersection.vo
  • 36 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M5_Tactics.v
  • 35 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I3_OpposedAngles.vo
  • 34 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M3_SecantLines.vo
  • 34 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C3_SumDistance.glob
  • 34 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N5_UniqueParallel.glob
  • 33 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/K2_MidLineandRightAngle.glob
  • 33 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F4_ArchimedianDistance.vo
  • 33 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D4_DistanceLt.vo
  • 33 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G2_AngleProp.vo
  • 32 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/geom.vo
  • 31 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D3_SecondDimension.vo
  • 31 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H2_ParticularTriangles.glob
  • 30 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F2_MarkSegment.glob
  • 28 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N1_DrawingPerpendicularLines.glob
  • 27 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J3_MidProp.glob
  • 27 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C1_Distance.vo
  • 27 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L1_Parallelogramm.glob
  • 27 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B5_BetweenProp.glob
  • 26 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L3_EquidirectedParallelogramm.glob
  • 24 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H1_Triangles.glob
  • 24 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C5_TriangularInequality.vo
  • 24 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/K1_RightAngle.glob
  • 23 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B4_RaysProp.glob
  • 22 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F1_IntersectionDiameterProp.glob
  • 19 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A3_Metrique.glob
  • 19 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M4_PerpendicularLines.glob
  • 18 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N4_DiscreteThales.glob
  • 18 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I1_SupplementaryAngle.glob
  • 18 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C1_Distance.glob
  • 18 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B3_EquiOrientedProp.vo
  • 17 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N6_ParallelAndPerpendicularLines.glob
  • 17 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D2_ExistsClockwise.vo
  • 16 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B5_BetweenProp.vo
  • 16 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E3_FourPointsIntersection.glob
  • 16 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M1_SuperImposedLines.glob
  • 16 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F3_Graduation.glob
  • 15 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E2_NotEquidirectedIntersection.glob
  • 14 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B4_RaysProp.vo
  • 14 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B6_EquiDirectedProp.vo
  • 14 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E1_IntersectionLinesProp.vo
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N3_ParallelOpposedLine.glob
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G1_Angles.v
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L5_nParallelogramm.glob
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L4_ParallelogrammAngles.v
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N2_DrawingParallelLine.glob
  • 12 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B6_EquiDirectedProp.glob
  • 12 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D1_IntersectionCirclesProp.vo
  • 12 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M2_ParallelLines.glob
  • 12 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D3_SecondDimension.v
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I3_OpposedAngles.glob
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C4_DistanceLe.glob
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A7_Tactics.vo
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A2_Orientation.glob
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J2_MidPoint.glob
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D1_IntersectionCirclesProp.glob
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I2_Supplement.v
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F4_ArchimedianDistance.glob
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C6_DistanceTimesN.glob
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H3_BuildingTriangle.glob
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G3_ParticularAngle.v
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N1_DrawingPerpendicularLines.v
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D4_DistanceLt.glob
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E1_IntersectionLinesProp.glob
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B2_CollinearProp.glob
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G2_AngleProp.glob
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C2_CircleAndDistance.vo
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C6_DistanceTimesN.vo
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A3_Metrique.vo
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M3_SecantLines.glob
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L2_StrictParallelogramm.v
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J1_MidLine.glob
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B2_CollinearProp.vo
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L3_EquidirectedParallelogramm.v
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C4_DistanceLe.vo
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C5_TriangularInequality.v
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A5_Cercle.vo
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N5_UniqueParallel.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A2_Orientation.vo
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B3_EquiOrientedProp.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D2_ExistsClockwise.glob
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H2_ParticularTriangles.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C3_SumDistance.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A4_Droite.vo
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J3_MidProp.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B1_ClockwiseProp.glob
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F2_MarkSegment.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B5_BetweenProp.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N4_DiscreteThales.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/K2_MidLineandRightAngle.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A7_Tactics.glob
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/K1_RightAngle.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B1_ClockwiseProp.vo
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L1_Parallelogramm.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B4_RaysProp.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C1_Distance.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F1_IntersectionDiameterProp.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A6_Intersection.vo
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A5_Cercle.glob
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H1_Triangles.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C2_CircleAndDistance.glob
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M4_PerpendicularLines.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N6_ParallelAndPerpendicularLines.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I1_SupplementaryAngle.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A6_Intersection.glob
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/geom.glob
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E3_FourPointsIntersection.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M2_ParallelLines.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N2_DrawingParallelLine.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F3_Graduation.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E2_NotEquidirectedIntersection.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A4_Droite.glob
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A7_Tactics.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M1_SuperImposedLines.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A1_Plan.vo
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B6_EquiDirectedProp.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J1_MidLine.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/L5_nParallelogramm.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A3_Metrique.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/J2_MidPoint.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D2_ExistsClockwise.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/N3_ParallelOpposedLine.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C4_DistanceLe.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/H3_BuildingTriangle.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D1_IntersectionCirclesProp.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C6_DistanceTimesN.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/G2_AngleProp.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/I3_OpposedAngles.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/D4_DistanceLt.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/F4_ArchimedianDistance.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/M3_SecantLines.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A2_Orientation.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B2_CollinearProp.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/geom.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/E1_IntersectionLinesProp.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A5_Cercle.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/B1_ClockwiseProp.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A4_Droite.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A6_Intersection.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/C2_CircleAndDistance.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A1_Plan.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/EuclideanGeometry/A1_Plan.v

Uninstall ๐Ÿงน

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