« Up

geocoq 2.2.1 1 h 15 m 🏆

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.5.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
# opam file:
opam-version: "2.0"
maintainer: "Julien Narboux <julien@narboux.fr>"
homepage: "http://geocoq.github.io/GeoCoq/"
bug-reports: "https://github.com/GeoCoq/GeoCoq/issues"
authors: ["Gabriel Braun <gabriel.braun@unistra.fr>" 
          "Pierre Boutry <pierre.boutry@unistra.fr>"
          "Charly Gries <Charly.Gries@etu.unistra.fr>"
          "Julien Narboux <narboux@unistra.fr>"]
license: "LGPL 3"
build: [
  ["./configure.sh"]
  [make "-j%{jobs}%"]
]
install: [
  [make "install"]
]
remove: ["rm" "-R" "%{lib}%/coq/user-contrib/GeoCoq"]
depends: [
  "ocaml"
  "coq"
    {((>= "8.4pl4" & < "8.5~") | (>= "8.5" & < "8.6~") |
      (>= "8.6" & < "8.7~"))}
]
tags: [
  "keyword:geometry"
  "keyword:neutral geometry"
  "keyword:euclidean geometry"
  "keyword:foundations"
  "keyword:Tarski"
  "keyword:Hilbert"
  "keyword:Pappus"
  "keyword:Desargues"
  "keyword:parallel postulates"
  "category:Mathematics/Geometry/General"
  "date:2016-12-22"
]
synopsis: "A formalization of foundations of geometry in Coq"
flags: light-uninstall
url {
  src: "https://github.com/GeoCoq/GeoCoq/archive/v2.2.1.tar.gz"
  checksum: "md5=be429fbeba560c84c994d551bb17c894"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-geocoq.2.2.1 coq.8.5.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 8h opam install -y --deps-only coq-geocoq.2.2.1 coq.8.5.2
Return code
0
Duration
1 m 0 s

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y -v coq-geocoq.2.2.1 coq.8.5.2
Return code
0
Duration
1 h 15 m

Installation size

Total: 46 M

  • 3 M ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Coplanar_trans.vo
  • 2 M ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates_with_functions.vo
  • 1 M ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_prod.vo
  • 1 M ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/midpoint_theorems.vo
  • 1 M ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/hilbert_to_tarski.vo
  • 1 M ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch11_angles.vo
  • 979 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates.vo
  • 956 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_sum.vo
  • 899 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Coplanar_trans.glob
  • 839 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch11_angles.glob
  • 821 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_1.vo
  • 813 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/gravityCenter.vo
  • 790 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/saccheri.vo
  • 748 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/Euclid.vo
  • 705 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals_inter_dec.vo
  • 613 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/orientation.vo
  • 607 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_6_Desargues_Hessenberg.vo
  • 584 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_lengths.vo
  • 546 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates_with_functions.glob
  • 517 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/hilbert_to_tarski.glob
  • 489 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch08_orthogonality.vo
  • 399 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/project.vo
  • 389 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/suma.vo
  • 388 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals_inter_dec.glob
  • 377 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_sum.glob
  • 376 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Utils/sets.vo
  • 375 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/ColR.vo
  • 368 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_tarski.vo
  • 357 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/legendre.vo
  • 344 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Coplanar_trans.v
  • 342 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/saccheri.glob
  • 331 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CoincR.vo
  • 330 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch09_plane.vo
  • 329 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_5_Pappus_Pascal.vo
  • 313 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals.vo
  • 313 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/vectors.vo
  • 297 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel_inter_dec.vo
  • 296 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/TCP_tarski.vo
  • 293 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/angle_archimedes.vo
  • 291 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/orientation.glob
  • 287 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates.glob
  • 287 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/suma.glob
  • 284 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_1.glob
  • 275 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_4_cos.vo
  • 271 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel.vo
  • 258 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch11_angles.v
  • 255 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_order.vo
  • 239 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch08_orthogonality.glob
  • 236 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/archimedes.vo
  • 233 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals.glob
  • 227 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_playfair_bis.vo
  • 222 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/posidonius_postulate_rah.vo
  • 219 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/orthocenter.vo
  • 210 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/circumcenter.vo
  • 206 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch09_plane.glob
  • 197 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_euclid.vo
  • 195 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/bisector.vo
  • 192 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Utils/arity.vo
  • 192 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_hilbert.vo
  • 188 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/universal_posidonius_postulate_par_perp_perp.vo
  • 187 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_lengths.glob
  • 182 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel.glob
  • 175 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/midpoint_playfair.vo
  • 173 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_existential_inverse_projection_postulate.vo
  • 173 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_3_angles.vo
  • 170 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_prod.glob
  • 170 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_4_cos.glob
  • 170 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_proclus.vo
  • 168 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity.vo
  • 167 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/ColR.glob
  • 163 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/Euler_line.vo
  • 157 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity_2D.vo
  • 156 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_pyth_rel.vo
  • 156 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim.vo
  • 154 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/varignon.vo
  • 153 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/vectors.glob
  • 149 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/project.glob
  • 145 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/incenter.vo
  • 142 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_order.glob
  • 141 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_6_Desargues_Hessenberg.glob
  • 140 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_beeson.vo
  • 139 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Utils/arity.glob
  • 139 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_5_Pappus_Pascal.glob
  • 139 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CoincR.glob
  • 137 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_NID.vo
  • 135 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/euclid_5_original_euclid.vo
  • 132 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel_inter_dec.glob
  • 127 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/Euclid.glob
  • 127 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_playfair.vo
  • 125 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/inverse_projection_postulate_proclus_bis.vo
  • 123 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_inverse_projection_postulate_legendre_s_postulate.vo
  • 123 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/Euclid_def.vo
  • 122 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_hilbert.glob
  • 122 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tarski_to_coinc_theory_for_concyclic.vo
  • 121 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/hilbert_to_tarski.v
  • 120 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity.glob
  • 118 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Axioms/hilbert_axioms.vo
  • 116 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/similar_rah.vo
  • 116 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/szmielew.vo
  • 113 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_spp_inverse_projection_postulate.vo
  • 113 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_euclid_original_spp.vo
  • 112 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Utils/sets.glob
  • 110 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests.vo
  • 109 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_universal_posidonius_postulate.vo
  • 108 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_3_angles.glob
  • 107 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/exercises.vo
  • 106 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/concyclic.vo
  • 106 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_sum.v
  • 106 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/legendre.glob
  • 106 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_aristotle.vo
  • 106 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom.vo
  • 104 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_2_length.vo
  • 103 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_bet_identity.vo
  • 102 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/midpoint_thales.vo
  • 102 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals_inter_dec.v
  • 101 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity_2D.glob
  • 100 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch07_midpoint.vo
  • 100 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_playfair_rah.vo
  • 99 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_bis_proclus.vo
  • 99 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates.v
  • 98 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_playfair_bis.vo
  • 95 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Coplanar_perm.vo
  • 95 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/perp_bisect.vo
  • 93 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_playfair.vo
  • 92 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/triangles.vo
  • 90 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_similar.vo
  • 89 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch07_midpoint.glob
  • 89 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/archimedes.glob
  • 89 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/independent_tarski_to_tarski.vo
  • 89 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/saccheri.v
  • 87 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_postulate_thales_converse_postulate.vo
  • 87 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/aristotle_greenberg.vo
  • 86 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Decidability/equivalence_between_decidability_properties_of_basic_relations.glob
  • 85 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/angle_archimedes.glob
  • 84 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Decidability/equivalence_between_decidability_properties_of_basic_relations.vo
  • 84 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch06_out_lines.glob
  • 84 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_posidonius_postulate.vo
  • 84 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_triangle.vo
  • 82 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/consecutive_interior_angles_alternate_interior_angles.vo
  • 82 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/Tagged_predicates.vo
  • 82 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_TCP.vo
  • 82 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_1.v
  • 81 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_s_euclid_remove_degenerated_cases.vo
  • 80 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests_2.vo
  • 79 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_midpoint.vo
  • 79 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch06_out_lines.vo
  • 78 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CoincR_for_col.vo
  • 78 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_consecutive_interior_angles.vo
  • 78 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_ID.vo
  • 78 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_triangle_circumscription_principle.vo
  • 76 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_2_par_par_perp_perp.vo
  • 76 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tarski_to_coinc_theory_for_cop.vo
  • 76 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/Euclid_def.glob
  • 74 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_alternate_interior_angles.vo
  • 73 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_bis_playfair.vo
  • 73 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_SPP.vo
  • 73 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_existential_triangle.vo
  • 73 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/orientation.v
  • 73 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_par_trans.vo
  • 73 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_thales_existence.vo
  • 72 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_principle_rectangle_existence.vo
  • 72 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_playfair.vo
  • 72 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_existence_rah.vo
  • 72 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_triangle_rah.vo
  • 72 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_weak_triangle_circumscription_principle.vo
  • 72 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_prod.v
  • 72 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_existential_playfair.vo
  • 72 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_existence_rah.vo
  • 71 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_existential_saccheri.vo
  • 71 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_saccheri_rah.vo
  • 71 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_thales_postulate.vo
  • 71 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_par_perp_2_par.vo
  • 71 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_rectangle_principle.vo
  • 71 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_triangle.vo
  • 71 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/TCP_tarski.glob
  • 70 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/circumcenter.glob
  • 69 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/suma.v
  • 69 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch09_plane.v
  • 66 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch05_bet_le.glob
  • 65 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch08_orthogonality.v
  • 63 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates_with_functions.v
  • 62 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_order.v
  • 61 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim.glob
  • 60 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_beeson.glob
  • 60 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_pyth_rel.glob
  • 60 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/midpoint_theorems.glob
  • 58 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/independent_tarski_to_tarski.glob
  • 57 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_bet_identity.glob
  • 56 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/ColR.v
  • 56 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch05_bet_le.vo
  • 53 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel.v
  • 51 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_6_Desargues_Hessenberg.v
  • 51 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_4_cos.v
  • 50 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_lengths.v
  • 50 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals.v
  • 50 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/bisector.glob
  • 47 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel_inter_dec.v
  • 46 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tactics_axioms.vo
  • 45 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tarski_to_coinc_theory_for_concyclic.glob
  • 44 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_5_Pappus_Pascal.v
  • 41 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/orthocenter.glob
  • 41 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/gravityCenter.glob
  • 41 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/triangles.glob
  • 40 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/vectors.v
  • 39 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch03_bet.glob
  • 39 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Utils/arity.v
  • 39 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch03_bet.vo
  • 39 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/project.v
  • 38 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tarski_to_coinc_theory_for_col.vo
  • 38 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch02_cong.glob
  • 38 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CoincR.v
  • 37 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_tarski.glob
  • 37 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity.v
  • 34 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Axioms/beeson_s_axioms.vo
  • 34 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Utils/sets.v
  • 33 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch02_cong.vo
  • 32 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/Permutations.vo
  • 32 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests_2.glob
  • 32 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Axioms/hilbert_axioms.glob
  • 31 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_3_angles.v
  • 31 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tarski_to_col_theory.vo
  • 30 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests.glob
  • 30 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_col.vo
  • 30 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_NID.glob
  • 29 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity_2D.v
  • 29 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_col.glob
  • 29 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_2_length.glob
  • 28 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/Euler_line.glob
  • 28 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Axioms/independent_tarski_axioms.vo
  • 26 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch07_midpoint.v
  • 26 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/legendre.v
  • 25 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/circumcenter.v
  • 25 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Axioms/tarski_axioms.vo
  • 25 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/varignon.glob
  • 24 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/perp_bisect.glob
  • 23 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_playfair_bis.glob
  • 23 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_makarios.glob
  • 23 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/posidonius_postulate_rah.glob
  • 23 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_hilbert.v
  • 23 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/concyclic.glob
  • 21 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/Euclid.v
  • 21 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/archimedes.v
  • 21 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/gravityCenter.v
  • 20 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/Tagged_predicates.glob
  • 20 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/similar_rah.glob
  • 20 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch06_out_lines.v
  • 20 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Utils/all_equiv.vo
  • 20 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/angle_archimedes.v
  • 20 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_segment_construction.glob
  • 19 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/universal_posidonius_postulate_par_perp_perp.glob
  • 18 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Axioms/independent_tarski_axioms.glob
  • 17 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Axioms/makarios_variant_axioms.vo
  • 17 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim.v
  • 17 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_pyth_rel.v
  • 17 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/TCP_tarski.v
  • 17 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Coplanar_perm.glob
  • 16 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_cong_bet.vo
  • 16 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/bisector.v
  • 16 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_proclus.glob
  • 15 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/incenter.glob
  • 15 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_euclid.glob
  • 14 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_playfair.glob
  • 14 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/Euler_line.v
  • 14 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/exercises.glob
  • 14 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_cong_bet.glob
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Decidability/equivalence_between_decidability_properties_of_basic_relations.v
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_beeson.v
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CoincR_for_col.glob
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_aristotle.glob
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_existential_inverse_projection_postulate.glob
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch05_bet_le.v
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_makarios.vo
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/orthocenter.v
  • 12 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Axioms/beeson_s_axioms.glob
  • 12 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/midpoint_playfair.glob
  • 12 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Axioms/tarski_axioms.glob
  • 12 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_tarski.v
  • 12 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Utils/general_tactics.vo
  • 12 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_2_length.v
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/szmielew.glob
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/independent_tarski_to_tarski.v
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_s_euclid_remove_degenerated_cases.glob
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/aristotle_greenberg.glob
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tarski_to_coinc_theory_for_concyclic.v
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_segment_construction.vo
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_posidonius_postulate.glob
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch03_bet.v
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_playfair_bis.glob
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/midpoint_theorems.v
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tactics_axioms.glob
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tarski_to_coinc_theory_for_cop.glob
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tarski_to_coinc_theory_for_col.glob
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Axioms/makarios_variant_axioms.glob
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_universal_posidonius_postulate.glob
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/posidonius_postulate_rah.v
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_playfair_bis.v
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/Euclid_def.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch02_cong.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/similar_rah.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/exercises.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_NID.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/inverse_projection_postulate_proclus_bis.glob
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_spp_inverse_projection_postulate.glob
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_TCP.glob
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_inverse_projection_postulate_legendre_s_postulate.glob
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/Permutations.glob
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/triangles.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/varignon.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/universal_posidonius_postulate_par_perp_perp.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_postulate_thales_converse_postulate.glob
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_euclid.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Utils/aux.vo
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_col.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/euclid_5_original_euclid.glob
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/midpoint_playfair.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/incenter.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/concyclic.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/perp_bisect.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_similar.glob
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_playfair_rah.glob
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/midpoint_thales.glob
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_existential_inverse_projection_postulate.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_euclid_original_spp.glob
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Coplanar_perm.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_proclus.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Utils/all_equiv.glob
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_bet_identity.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Utils/general_tactics.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_triangle_circumscription_principle.glob
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_playfair.glob
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/CoincR_for_col.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_triangle.glob
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_aristotle.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_makarios.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests_2.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom.glob
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_playfair.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Axioms/hilbert_axioms.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_bis_proclus.glob
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Utils/general_tactics.glob
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_universal_posidonius_postulate.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/Tagged_predicates.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/szmielew.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/consecutive_interior_angles_alternate_interior_angles.glob
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_TCP.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_euclid_original_spp.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_inverse_projection_postulate_legendre_s_postulate.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/inverse_projection_postulate_proclus_bis.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_playfair_bis.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_posidonius_postulate.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_spp_inverse_projection_postulate.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/aristotle_greenberg.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_consecutive_interior_angles.glob
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_cong_bet.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_s_euclid_remove_degenerated_cases.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/euclid_5_original_euclid.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_ID.glob
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_playfair.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tarski_to_coinc_theory_for_col.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_midpoint.glob
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Highschool/midpoint_thales.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/Permutations.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_playfair_rah.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_alternate_interior_angles.glob
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_postulate_thales_converse_postulate.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_similar.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tarski_to_coinc_theory_for_cop.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_par_trans.glob
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Axioms/tarski_axioms.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_bis_playfair.glob
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tactics_axioms.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Axioms/independent_tarski_axioms.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_thales_existence.glob
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_segment_construction.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_2_par_par_perp_perp.glob
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_triangle_circumscription_principle.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_triangle.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/consecutive_interior_angles_alternate_interior_angles.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Axioms/beeson_s_axioms.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_bis_proclus.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tarski_to_col_theory.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Utils/all_equiv.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_ID.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_weak_triangle_circumscription_principle.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Axioms/makarios_variant_axioms.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_principle_rectangle_existence.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_existential_triangle.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_consecutive_interior_angles.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_2_par_par_perp_perp.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_par_perp_2_par.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Utils/aux.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_SPP.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_triangle_rah.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_par_trans.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_saccheri_rah.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_existence_rah.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_bis_playfair.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_rectangle_principle.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_midpoint.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_existence_rah.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_thales_postulate.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_existential_saccheri.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_playfair.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_existential_playfair.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_triangle.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_alternate_interior_angles.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_thales_existence.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_principle_rectangle_existence.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_weak_triangle_circumscription_principle.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_existential_triangle.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Tactics/Coinc/tarski_to_col_theory.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_existential_saccheri.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_SPP.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_existential_playfair.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_par_perp_2_par.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_triangle_rah.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_saccheri_rah.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_playfair.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_existence_rah.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_existence_rah.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Utils/aux.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_rectangle_principle.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_thales_postulate.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_triangle.v

Uninstall 🧹

Command
opam remove -y coq-geocoq.2.2.1
Return code
0
Missing removes
none
Wrong removes
none

Sources are on GitHub © Guillaume Claret 🐣