# 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: [
"Jim Portegies"
"Cosmin Manea"
"Lulof Pirée"
"Adrian Vrămuleţ"
"Tudor Voicu"
]
license: "LGPL 3.0"
depends: [
"coq" {>= "8.12" & < "8.14"}
]
build: [
[make "-j%{jobs}%"]
]
install: [
[make "install"]
]
url {
src: "https://github.com/impermeable/coq-waterproof/archive/1.0.0.tar.gz"
checksum: "sha256=bc2e6ec7b458ad491b7bf95186d1b440240ee5cc4c449feea002b53e9bb60ae9"
}
tags: [
"keyword:mathematics education"
"category:Math/Education"
"date:2021-06-24"
"logpath:Waterproof"
]
trueDry install with the current Coq version:
opam install -y --show-action coq-waterproof.1.0.0 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.0.0 coq.8.13.1opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-waterproof.1.0.0 coq.8.13.1Total: 3 M
../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/databases.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/rewrite_inequalities_test.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/definitions/subsequences.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/rewrite_inequalities.vo../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/test/test_tactics/test_forward_reasoning/rewrite_using_test.vo../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_forward_reasoning/write_using_test.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/test/test_tactics/test_forward_reasoning/we_conclude_that_test.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/tactics/sets_tactics/sets_automation_tactics.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/tactics/automation_databases/decidability_db.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/tactics/forward_reasoning/rewrite_using.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/proof_finishing_tactics_test.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/proof_finishing_tactics.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_forward_reasoning/write_as_test.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/tactics/forward_reasoning/it_suffices_to_show.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/tactics/forward_reasoning/write_using.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/test/test_tactics/take_test.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/tactics/forward_reasoning/write_as.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/notations/set_notations.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/load_database/All.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/test/test_tactics/test_choose_such_that.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_contradiction_tactics/test_basic_contradiction.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/test/test_tactics/test_either.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/contradiction_tactics/basic_contradiction.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/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/RealsAndIntegers.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/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/SquareRoot.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/reals.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Other.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/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/test/test_tactics/rewrite_inequalities_test.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/rewrite_using_test.glob../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/tactics/rewrite_inequalities.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_know.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/definitions/subsequences.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/databases.v../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/test/test_load_database.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/rewrite_inequalities_test.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/tactics/assume.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/write_using_test.glob../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/test/test_tactics/take_test.glob../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/tactics/assume.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_auxiliary.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/automation_databases/decidability_db.glob../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/tactics/forward_reasoning/rewrite_using.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/proof_finishing_tactics_test.glob../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/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/test/test_tactics/test_we_show_both_statements.vo../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/auxiliary.v../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/notations/notations.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/write_using.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/auxiliary.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/test/test_tactics/we_need_to_show_test.vo../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/forward_reasoning/it_suffices_to_show.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/tactics/we_show_both_statements.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/rewrite_using_test.v../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/definitions/subsequences.v../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/selected_databases.v../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/test/test_tactics/test_forward_reasoning/we_conclude_that_test.v../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/sets_tactics/sets_automation_tactics.v../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/we_know.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/string_auxiliary_test.vo../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/we_need_to_show.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/test/test_tactics/test_forward_reasoning/test_induction.vo../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/tactics/take.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/tactics/choose_such_that.vo../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/proof_finishing_tactics_test.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/tactics/goal_to_hint.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_apply.vo../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_auxiliary_test.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/simplify.vo../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/induction.vo../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/tactics/forward_reasoning/define.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_know.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/automation_databases/decidability_db.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_tactics/test_because.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/test/test_tactics/test_choose_such_that.glob../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/apply.vo../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_we_show_both_directions.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/proof_finishing_tactics.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/test/test_tactics/test_forward_reasoning/test_simplify.vo../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/write_using_test.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/test_forward_reasoning/it_suffices_to_show_test.v../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/test/test_set_search_depth.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_know.v../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/forward_reasoning/write_as.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/tactics/we_need_to_show.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_auxiliary_test.glob../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/tactics/we_know.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/such_that_test.v../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/reverse_engineer/auto_hintdb_arg.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/rewrite_inequalities.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_choose_such_that.v../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/test/test_tactics/unfold_test.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/contradiction_tactics/basic_contradiction.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/tactics/either.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/test_choose.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/AllTactics.glob../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/notations/set_notations.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/write_as_test.glob../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_tactics/goal_to_hint_test.v../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/notations/set_notations.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/load_database/All.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/test_tactics/test_forward_reasoning/test_apply.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/write_as_test.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_forward_reasoning/test_apply.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_set_intuition.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_simplify.glob../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_either.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_contradiction_tactics/test_basic_contradiction.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_contradiction_tactics/test_basic_contradiction.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_forward_reasoning/test_define.v../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/tactics/forward_reasoning/apply.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/definitions/set_definitions.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_simplify.v../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/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/RealsAndIntegers.v../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/Multiplication.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/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/SquareRoot.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/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/Sets.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/ZeroOne.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Other.v../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/reals.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/tactics/forward_reasoning/forward_reasoning_aux.glob../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/tactics/sets_tactics/sets_automation_tactics.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/simplify.v../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/we_conclude_that.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/tactics/either.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/contradiction_tactics/basic_contradiction.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/test_auxiliary.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/tactics/choose.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/tactics/forward_reasoning/rewrite_using.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/selected_databases.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/tactics/forward_reasoning/it_holds_that.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/write_as.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/forward_reasoning/proof_finishing_tactics.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/we_know.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/write_using.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/tactics/we_show_both_directions.glob../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/tactics/take.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/tactics/unfold.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/RealsAndIntegers.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/PlusMinus.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/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/ZeroOne.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/load_database/Sets.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/Other.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/load_database/reals.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/choose_such_that.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/string_auxiliary.glob../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/tactics/forward_reasoning/simplify.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/apply.glob../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Waterproof/tactics/because.globopam remove -y coq-waterproof.1.0.0