# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq 8.13.1 Formal proof management system
num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.12.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.12.1 Official release 4.12.1
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.6 A library manager for OCaml
zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
synopsis: "Waterproof library"
description: """
The Waterproof library provides tactics, notations, and mathematical theories geared towards use in Mathematics educational environments. It aims to provide syntax such that proof scripts mimic handwritten mathematical proofs.
"""
homepage: "https://github.com/impermeable/coq-waterproof"
dev-repo: "git+https://github.com/impermeable/coq-waterproof.git"
bug-reports: "https://github.com/impermeable/coq-waterproof/issues"
maintainer: "j.w.portegies@tue.nl"
authors: [
"Jelle Wemmenhove"
"Cosmin Manea"
"Lulof Pirée"
"Adrian Vrămuleţ"
"Tudor Voicu"
"Jim Portegies"
]
license: "LGPL 3.0"
depends: [
"coq" {>= "8.13" & < "8.16"}
]
build: [
[make "-j%{jobs}%"]
]
install: [
[make "install"]
]
url {
src: "https://github.com/impermeable/coq-waterproof/archive/1.1.2.tar.gz"
checksum: "sha256=aac7996c3b40804e6c4db78ef6c8d2ceed2783774a859af8452cc680d1dc79bc"
}
tags: [
"keyword:mathematics education"
"category:Mathematics/Education"
"date:2022-02-03"
"logpath:Waterproof"
]
trueDry install with the current Coq version:
opam install -y --show-action coq-waterproof.1.1.2 coq.8.13.1Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-waterproof.1.1.2 coq.8.13.1opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-waterproof.1.1.2 coq.8.13.1Total: 5 M
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/sup_and_inf_new_definitions.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/sequences.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_databases/test_waterproof_integers_database.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_databases/test_reals_database.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/databases.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/limsup_liminf_bolzano.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/sequences.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_manipulate_negation.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/sup_and_inf.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/subsequences.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/sup_and_inf_new_definitions.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_goal_wrappers.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_manipulate_negation.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/limsup_liminf_bolzano.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_inequality_chains.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/subsequences.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/definitions/inequality_chains.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/waterprove/manipulate_negation.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/subsequences_metric.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/sup_and_inf.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/series.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_databases/test_waterproof_integers_database.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/waterprove/manipulate_negation.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/we_conclude_that_test.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_databases/test_reals_database.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_sets_tactics/test_sets_automation_tactics.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_either.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/either.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_load_database.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/metric_spaces.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_shield_automation.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/it_holds_that_test.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_set_definitions.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/databases.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/notations/notations.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/sequential_accumulation_points.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/sets_tactics/sets_automation_tactics.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/subsequences_metric.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_contradiction.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/we_conclude_that.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_because.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/because.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_goal_wrappers.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_choose_such_that.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/AllTactics.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/it_suffices_to_show_test.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/AllConstructiveTactics.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_simplify_chains.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/take_test.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/it_holds_that.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/it_suffices_to_show.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/selected_databases.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/waterprove/automation_subroutine.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/waterprove/waterprove.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/notations/set_notations.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_set_search_depth.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/All.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/simplify_chains.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/forward_reasoning_aux.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_set_intuition.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/series.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_shield_automation.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/RealsAndIntegers.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/RealNumbers.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/sequences_metric.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/DisableWildcard.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/EnableWildcard.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_intuition/Disabled.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_intuition/Enabled.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Integers.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/sup_and_inf_new_definitions.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/ConstructiveLogic.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Multiplication.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/ClassicalLogic.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/AbsoluteValue.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Exponential.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Additional.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Firstorder.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/SquareRoot.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Intuition.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/PlusMinus.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/ZeroOne.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Subsets.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Sets.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/definitions/set_definitions.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_search_depth/To_2.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_search_depth/To_4.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_search_depth/To_1.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_search_depth/To_5.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_search_depth/To_3.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/databases.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_load_database.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_either.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/sequences.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/goal_wrappers.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_inequality_chains.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/sup_and_inf.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/goal_wrappers.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/definitions/inequality_chains.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/limsup_liminf_bolzano.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_choose_such_that.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/subsequences.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_because.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_load_database.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/unfold_test.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/waterprove/manipulate_negation.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/take_test.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/assume_test.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/goal_to_hint_test.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/contradiction.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/sequential_accumulation_points.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/metric_spaces.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/either.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_show_both_statements.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_show_both_statements.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_induction.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/definitions/inequality_chains.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/unfold.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test_auxiliary.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/we_need_to_show_test.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/auxiliary.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/subsequences_metric.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/induction.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/such_that_test.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/choose_such_that.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/we_conclude_that.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/assume_test.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/auxiliary.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/we_show_both_statements.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/we_conclude_that_test.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/notations/notations.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/assume.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_auxiliary_test.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/selected_databases.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test_auxiliary.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/string_auxiliary.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/either.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/it_suffices_to_show.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_choose.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/assume.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/series.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/waterprove/automation_subroutine.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/we_need_to_show.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_sets_tactics/test_sets_automation_tactics.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/goal_to_hint.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/take.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_set_definitions.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/unfold_test.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/unfold.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_manipulate_negation.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/we_show_both_statements.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/notations/notations.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/goal_wrappers.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/we_conclude_that_test.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/choose.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/take.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/we_need_to_show.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/because.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_show_both_directions.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/goal_to_hint.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/we_show_both_directions.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/string_auxiliary_test.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/string_auxiliary.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/sets_tactics/sets_automation_tactics.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/it_holds_that_test.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_shield_automation.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/take_test.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/it_holds_that.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_define.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/define.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/waterprove/waterprove.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_claims.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/it_suffices_to_show_test.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/claims.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/choose_such_that.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/induction.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_choose.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/it_holds_that_test.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/assume_test.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/sequences_metric.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_auxiliary_test.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/such_that_test.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_either.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_because.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/reverse_engineer/auto_hintdb_arg.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/it_suffices_to_show_test.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_choose_such_that.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_set_definitions.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/goal_to_hint_test.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_show_both_directions.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_show_both_statements.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/choose.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/forward_reasoning_aux.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/unfold_test.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_sets_tactics/test_sets_automation_tactics.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_set_search_depth.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_auxiliary_test.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/sequential_accumulation_points.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/goal_to_hint_test.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/metric_spaces.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/string_auxiliary_test.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_induction.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/we_need_to_show_test.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/such_that_test.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/we_show_both_directions.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/we_need_to_show_test.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/reverse_engineer/auto_hintdb_arg.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/AllTactics.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_define.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_goal_wrappers.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/AllConstructiveTactics.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_contradiction.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_choose.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/contradiction.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/simplify_chains.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_set_search_depth.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_induction.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/notations/set_notations.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_set_intuition.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_databases/test_waterproof_integers_database.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_show_both_directions.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_simplify_chains.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/All.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_contradiction.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/notations/set_notations.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_claims.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/define.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_simplify_chains.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_inequality_chains.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_claims.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/RealsAndIntegers.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/claims.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/RealNumbers.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_set_intuition.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/AllTactics.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/definitions/set_definitions.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_databases/test_reals_database.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_define.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Integers.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/AllConstructiveTactics.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/sets_tactics/sets_automation_tactics.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/we_conclude_that.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/EnableWildcard.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/DisableWildcard.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_intuition/Disabled.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_intuition/Enabled.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/ClassicalLogic.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Multiplication.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/AbsoluteValue.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Exponential.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/ConstructiveLogic.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/SquareRoot.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Additional.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/PlusMinus.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Sets.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_search_depth/To_1.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_search_depth/To_3.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_search_depth/To_5.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_search_depth/To_2.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_search_depth/To_4.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/ZeroOne.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Firstorder.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Intuition.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Subsets.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/induction.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/definitions/set_definitions.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/goal_to_hint.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/unfold.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/All.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/auxiliary.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/theory/analysis/sequences_metric.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/we_need_to_show.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/waterprove/waterprove.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test_auxiliary.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/we_show_both_statements.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/choose.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/simplify_chains.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/choose_such_that.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/assume.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/it_holds_that.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/because.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/forward_reasoning_aux.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/we_show_both_directions.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/it_suffices_to_show.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/string_auxiliary_test.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/waterprove/automation_subroutine.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/take.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/selected_databases.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/define.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/contradiction.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/claims.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_intuition/Disabled.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_intuition/Enabled.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/reverse_engineer/auto_hintdb_arg.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/DisableWildcard.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/EnableWildcard.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/ConstructiveLogic.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/RealsAndIntegers.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/ClassicalLogic.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Multiplication.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/AbsoluteValue.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Exponential.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/SquareRoot.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Additional.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/RealNumbers.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/PlusMinus.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Firstorder.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_search_depth/To_4.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_search_depth/To_5.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_search_depth/To_1.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_search_depth/To_3.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/set_search_depth/To_2.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Intuition.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Integers.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/ZeroOne.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Subsets.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Sets.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/string_auxiliary.globopam remove -y coq-waterproof.1.1.2