# Packages matching: installed # Name # Installed # Synopsis base-bigarray base 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.8.0 Formal proof management system num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.07.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.07.1 Official release 4.07.1 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.6 A library manager for OCaml # opam file: opam-version: "2.0" synopsis: "A formalization of foundations of geometry in Coq" description: "This subpackage contains the main developments from Hilbert's and Tarski's axiom systems." maintainer: "Julien Narboux <julien@narboux.fr>" authors: ["Gabriel Braun <gabriel.braun@unistra.fr>" "Pierre Boutry <pierre.boutry@inria.fr>" "Charly Gries <charly.gries@etu.unistra.fr>" "Julien Narboux <narboux@unistra.fr>" "Pascal Schreck <schreck@unistra.fr>"] license: "LGPL 3" homepage: "http://geocoq.github.io/GeoCoq/" bug-reports: "https://github.com/GeoCoq/GeoCoq/issues" dev-repo: "git+https://github.com/GeoCoq/GeoCoq.git" depends: [ "coq-geocoq-axioms" { = "2.4.0" } ] build: [ ["mkdir" "main/"] ["mv" "main.v" "main/"] ["./configure-main.sh"] [make "-j%{jobs}%"] ] install: [[make "install"]] tags: [ "keyword:geometry" "keyword:neutral geometry" "keyword:euclidean geometry" "keyword:foundations" "keyword:Tarski" "keyword:Hilbert" "keyword:Euclid" "keyword:Pappus" "keyword:Desargues" "keyword:arithmetization" "keyword:Pythagoras" "keyword:Thales' intercept theorem" "keyword:continuity" "keyword:ruler and compass" "keyword:parallel postulates" "category:Mathematics/Geometry/General" "date:2018-06-13" ] extra-files: [["Make.in" "md5=ee7f1852debd8d9621ebafa3c8b25dcc"]] url { src: "https://github.com/GeoCoq/GeoCoq/archive/v2.4.0.tar.gz" checksum: "md5=4a4ad33b4cad9b815a9b5c6308524c63" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-geocoq-main.2.4.0 coq.8.8.0
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
true
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-geocoq-main.2.4.0 coq.8.8.0
opam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y -v coq-geocoq-main.2.4.0 coq.8.8.0
Total: 50 M
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates_with_functions.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch11_angles.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_prod.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/hilbert_to_tarski.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/midpoint_theorems.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch11_angles.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_lengths.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_1.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_sum.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_6_Desargues_Hessenberg.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals_inter_dec.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/saccheri.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/gravityCenter.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/orientation.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch09_plane.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/hilbert_to_tarski.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch08_orthogonality.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates_with_functions.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/suma.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_euclid.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/universal_posidonius_postulate_par_perp_perp.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_inverse_projection_postulate_bachmann_s_lotschnittaxiom.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_tarski.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/project.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals_inter_dec.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/TCP_tarski.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_sum.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_legendre_s_parallel_postulate.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_5_Pappus_Pascal.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/saccheri.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/suma.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_lengths.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/circles.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_playfair_bis.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch09_plane.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/vectors.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/parallel_postulates.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch11_angles.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/angle_archimedes.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/orientation.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/inscribed_angle.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_1.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_order.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_4_cos.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/legendre.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch08_orthogonality.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_proclus.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/orthocenter.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/inverse_projection_postulate_proclus_bis.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/sesamath_exercises.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_inverse_projection_postulate.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_hilbert.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/posidonius_postulate_rah.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/circumcenter.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/archimedes.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_euclid.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/circles.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/first_order_dedekind_circle_circle.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/tangency.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity_2.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/bisector.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_NID.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch07_midpoint.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/midpoint_playfair.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_triangle_circumscription_principle.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/Euler_line.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/defect.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/elementary_continuity_props.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel_inter_dec.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Elements/Statements/Book_1.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_3_angles.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/varignon.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_pyth_rel.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_prod.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_tarski_s_parallel_postulate_weak_inverse_projection_postulate.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim_3.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/half_angles.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/aristotle.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/parallel_postulates.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_4_cos.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity_2.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_hilbert.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/incenter.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/vectors.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/inscribed_angle.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_playfair.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_inverse_projection_postulate_weak_tarski_s_parallel_postulate.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/hilbert_to_tarski.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_6_Desargues_Hessenberg.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/project.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_5_Pappus_Pascal.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_order.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_concyclic.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/euclid_5_original_euclid.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_playfair_bis.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/szmielew.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_completeness.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_bis_proclus.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_spp_inverse_projection_postulate.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch07_midpoint.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/concyclic.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/similar_rah.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/exercises.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_aristotle.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_playfair_rah.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_euclid_original_spp.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_universal_posidonius_postulate.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim_2.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/midpoint_thales.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_2_length.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_playfair.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/main.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_beeson.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/perp_bisect.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/grad.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_sum.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch06_out_lines.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/triangles.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals_inter_dec.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/completeness.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch09_plane.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_bet_identity.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Elements/Statements/Book_3.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/half_angles.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/rhombus.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_3_angles.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_similar.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch06_out_lines.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_postulate_thales_converse_postulate.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_bis_playfair.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests_2.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_lengths.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/ColR.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/saccheri.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_TCP.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_2_par_par_perp_perp.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_posidonius_postulate.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_triangle.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_SPP.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Elements/Statements/Book_1.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/Tagged_predicates.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_cop.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_archimedes.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Decidability/equivalence_between_decidability_properties_of_basic_relations.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Decidability/equivalence_between_decidability_properties_of_basic_relations.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/suma.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_col.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_ID.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_par_trans.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_midpoint.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/consecutive_interior_angles_alternate_interior_angles.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_consecutive_interior_angles.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_cop.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_alternate_interior_angles.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/TCP_tarski.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_par_perp_2_par.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_weak_triangle_circumscription_principle.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel_inter_dec.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_1.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch05_bet_le.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_existential_triangle.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_thales_existence.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/coplanar.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_continuous_to_trc.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_principle_rectangle_existence.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_existence_rah.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_triangle_rah.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_playfair.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_existential_saccheri.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_existence_rah.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_saccheri_rah.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_thales_postulate.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_rectangle_principle.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_triangle.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/orientation.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/angle_archimedes.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_prod.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/circumcenter.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch08_orthogonality.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch05_bet_le.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch16_coordinates_with_functions.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/first_order_dedekind_circle_circle.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch14_order.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/tangency.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_pyth_rel.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/sesamath_exercises.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_euclid.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/gupta_inspired_to_tarski.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/midpoint_theorems.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/sums.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_bet_identity.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/defect.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/sums.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/archimedes.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/beeson_to_tarski.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/gupta_inspired_to_tarski.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/coplanar.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_NID.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_6_Desargues_Hessenberg.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_concyclic.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_completeness.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/bisector.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim_3.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_legendre_s_parallel_postulate.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/circles.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_4_cos.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/elementary_continuity_props.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_5_Pappus_Pascal.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/legendre.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch03_bet.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/triangles.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/universal_posidonius_postulate_par_perp_perp.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/orthocenter.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/quadrilaterals.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_playfair_bis.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/gravityCenter.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_col.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests_2.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch03_bet.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/vectors.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/project.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/first_order.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_tarski.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch02_cong.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch07_midpoint.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Elements/Statements/Book_1.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_tarski_s_parallel_postulate_weak_inverse_projection_postulate.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/parallel_postulates.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim_2.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_inverse_projection_postulate.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_col_theory.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch02_cong.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_inverse_projection_postulate_weak_tarski_s_parallel_postulate.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_beeson.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch10_line_reflexivity_2.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_inverse_projection_postulate_bachmann_s_lotschnittaxiom.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/inscribed_angle.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_3_angles.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_col.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/grad.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/completeness.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/Euler_line.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_hilbert.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_triangle_circumscription_principle.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/perp_bisect.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_col.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/beeson_to_tarski.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_2_length.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/circumcenter.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch06_out_lines.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/varignon.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/posidonius_postulate_rah.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_s_euclid_remove_degenerated_cases.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/aristotle.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_proclus.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/gravityCenter.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/TCP_tarski.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/makarios_to_tarski.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/similar_rah.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/Tagged_predicates.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/concyclic.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_segment_construction.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/angle_archimedes.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/half_angles.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/rhombus.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_euclid.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/sesamath_exercises.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_gupta_inspired.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch15_pyth_rel.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/tangency.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_playfair_bis.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_playfair.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_cop.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/archimedes.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/bisector.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch05_bet_le.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_cong_bet.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/elementary_continuity_props.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/incenter.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch12_parallel_inter_dec.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/inverse_projection_postulate_proclus_bis.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/Euler_line.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/defect.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_aristotle.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/exercises.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/first_order_dedekind_circle_circle.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_col.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Elements/Statements/Book_3.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Decidability/equivalence_between_decidability_properties_of_basic_relations.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_euclid.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_playfair_bis.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/legendre.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/coplanar.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/orthocenter.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_cong_bet.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_completeness.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_legendre_s_parallel_postulate.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/sums.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_tarski.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/gupta_inspired_to_tarski.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_archimedes.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch13_2_length.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/midpoint_playfair.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_NID.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_s_euclid_remove_degenerated_cases.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/szmielew.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim_3.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_concyclic.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_posidonius_postulate.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/universal_posidonius_postulate_par_perp_perp.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_segment_construction.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/makarios_to_tarski.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_cop.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch03_bet.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_col.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/midpoint_theorems.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_gupta_inspired.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/first_order.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_universal_posidonius_postulate.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/posidonius_postulate_rah.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_playfair_rah.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Dimension_axioms/upper_dim_2.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/completeness.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/similar_rah.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch02_cong.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_spp_inverse_projection_postulate.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/grad.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/exercises.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_proclus.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_makarios.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/triangles.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/perp_bisect.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_beeson.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_inverse_projection_postulate_weak_tarski_s_parallel_postulate.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/beeson_to_tarski.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_playfair.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/aristotle.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_inverse_projection_postulate_bachmann_s_lotschnittaxiom.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_tarski_s_parallel_postulate_weak_inverse_projection_postulate.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_inverse_projection_postulate.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/rhombus.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/varignon.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_postulate_thales_converse_postulate.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_euclid.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/midpoint_playfair.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/ColR.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/euclid_5_original_euclid.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/incenter.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_col.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/concyclic.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_similar.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_euclid_original_spp.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/inverse_projection_postulate_proclus_bis.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/midpoint_thales.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_cop.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_bis_proclus.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_TCP.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/ColR.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_playfair_bis.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tactics/UnitTests/unit_tests_2.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_aristotle.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_bet_identity.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_makarios.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_triangle.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/bachmann_s_lotschnittaxiom_weak_triangle_circumscription_principle.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_par_trans.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Tactics/CoincR_for_col.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_playfair.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/dedekind_archimedes.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_existential_playfair.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_universal_posidonius_postulate.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Elements/Statements/Book_3.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_2_par_par_perp_perp.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/makarios_to_tarski.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_bis_playfair.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/szmielew.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Annexes/Tagged_predicates.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_posidonius_postulate.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_euclid_original_spp.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_playfair.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/original_spp_inverse_projection_postulate.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_makarios.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_TCP.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_playfair_rah.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/tarski_s_euclid_remove_degenerated_cases.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/euclid_5_original_euclid.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Continuity/first_order.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Tarski_dev/Ch04_cong_bet.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_ID.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_bis_proclus.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_cop.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_par_trans.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_midpoint.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_weak_triangle_circumscription_principle.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Highschool/midpoint_thales.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_coinc_theory_for_col.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_gupta_inspired.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_similar.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_postulate_thales_converse_postulate.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_alternate_interior_angles.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_bis_playfair.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_thales_existence.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_continuous_to_trc.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_consecutive_interior_angles.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Counter_models/counter_model_segment_construction.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_triangle.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/SPP_ID.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_2_par_par_perp_perp.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_col_theory.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_existential_playfair.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/consecutive_interior_angles_alternate_interior_angles.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_principle_rectangle_existence.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_SPP.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_existential_triangle.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_par_perp_2_par.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/consecutive_interior_angles_alternate_interior_angles.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_weak_triangle_circumscription_principle.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_triangle_rah.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_saccheri_rah.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_existence_rah.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/alternate_interior_angles_consecutive_interior_angles.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_rectangle_principle.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_midpoint.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_existence_rah.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_thales_postulate.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_existential_saccheri.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_alternate_interior_angles.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_converse_postulate_thales_existence.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_playfair.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_triangle.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_principle_rectangle_existence.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/proclus_SPP.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/triangle_existential_triangle.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_continuous_to_trc.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_perp_perp_par_perp_2_par.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_existential_saccheri.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_triangle_rah.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/existential_saccheri_rah.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Models/tarski_to_col_theory.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/par_trans_playfair.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rectangle_existence_rah.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/thales_existence_rah.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/playfair_existential_playfair.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_rectangle_principle.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_thales_postulate.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/main.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/Meta_theory/Parallel_postulates/rah_triangle.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/GeoCoq/main.glob
opam remove -y coq-geocoq-main.2.4.0