« Up

waterproof 1.0.0 1 m 51 s

(2021-10-22 16:55:43 UTC)

Context

# 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              3           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.0      The OCaml compiler (virtual package)
ocaml-base-compiler   4.12.0      Official release 4.12.0
ocaml-config          2           OCaml Switch Configuration
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special options enabled
ocamlfind             1.9.1       A library manager for OCaml
zarith                1.12        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"}
]
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"
]

Lint

Command
true
Return code
0

Dry install

Dry install with the current Coq version:

Command
opam install -y --show-action coq-waterproof.1.0.0 coq.8.13.1
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-waterproof.1.0.0 coq.8.13.1
Return code
0
Duration
8 s

Install

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-waterproof.1.0.0 coq.8.13.1
Return code
0
Duration
1 m 51 s

Installation size

Total: 3 M

  • 60 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/databases.vo
  • 51 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/rewrite_inequalities_test.vo
  • 49 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/definitions/subsequences.vo
  • 43 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/rewrite_inequalities.vo
  • 41 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/notations/notations.vo
  • 41 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/rewrite_using_test.vo
  • 40 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_sets_tactics/test_sets_automation_tactics.vo
  • 38 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/write_using_test.vo
  • 37 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_load_database.vo
  • 37 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/we_conclude_that_test.vo
  • 37 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/it_holds_that_test.vo
  • 35 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/sets_tactics/sets_automation_tactics.vo
  • 35 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/it_suffices_to_show_test.vo
  • 35 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/automation_databases/decidability_db.vo
  • 34 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/AllTactics.vo
  • 34 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/rewrite_using.vo
  • 34 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/proof_finishing_tactics_test.vo
  • 33 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/proof_finishing_tactics.vo
  • 33 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/we_conclude_that.vo
  • 32 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/write_as_test.vo
  • 32 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/definitions/set_definitions.vo
  • 32 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/it_suffices_to_show.vo
  • 32 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/waterprove/waterprove.vo
  • 32 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/write_using.vo
  • 32 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/it_holds_that.vo
  • 32 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/take_test.vo
  • 31 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/databases.glob
  • 31 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/write_as.vo
  • 31 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/forward_reasoning_aux.vo
  • 31 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/notations/set_notations.vo
  • 31 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/selected_databases.vo
  • 31 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/All.vo
  • 31 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_set_search_depth.vo
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_choose_such_that.vo
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_contradiction_tactics/test_basic_contradiction.vo
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_set_intuition.vo
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_either.vo
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/contradiction_tactics/basic_contradiction.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/either.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/DisableWildcard.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/EnableWildcard.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_intuition/Disabled.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_intuition/Enabled.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/RealsAndIntegers.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/Multiplication.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/AbsoluteValue.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/Exponential.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/Additional.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/SquareRoot.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/PlusMinus.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/ZeroOne.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/reals.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/Other.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/Sets.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_2.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_4.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_1.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_5.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_3.vo
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/rewrite_inequalities_test.glob
  • 23 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/rewrite_using_test.glob
  • 19 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_load_database.glob
  • 19 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/rewrite_inequalities.v
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_know.vo
  • 15 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/definitions/subsequences.glob
  • 15 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/assume_test.glob
  • 14 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/databases.v
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/notations/notations.glob
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_load_database.v
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/rewrite_inequalities_test.v
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/assume_test.vo
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/assume.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/write_using_test.glob
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/such_that_test.vo
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/take_test.glob
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/assume_test.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/assume.vo
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_show_both_statements.glob
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test_auxiliary.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/automation_databases/decidability_db.glob
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/waterprove/waterprove.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/rewrite_using.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/proof_finishing_tactics_test.glob
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_auxiliary_test.vo
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test_auxiliary.vo
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/string_auxiliary.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_show_both_statements.vo
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/we_show_both_statements.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/auxiliary.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/we_conclude_that.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/notations/notations.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/write_using.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/auxiliary.vo
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_sets_tactics/test_sets_automation_tactics.glob
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/we_need_to_show_test.vo
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_choose.vo
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/it_suffices_to_show.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/unfold_test.vo
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/we_show_both_statements.vo
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/rewrite_using_test.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_because.vo
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/definitions/subsequences.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/because.vo
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/selected_databases.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/we_conclude_that_test.glob
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/we_conclude_that_test.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/goal_to_hint_test.vo
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/sets_tactics/sets_automation_tactics.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/goal_to_hint.vo
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/we_know.vo
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/take.vo
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/string_auxiliary_test.vo
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/choose.vo
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/we_need_to_show.vo
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/string_auxiliary.vo
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_induction.vo
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/unfold.vo
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/take.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/we_show_both_directions.vo
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/choose_such_that.vo
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/it_holds_that.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/proof_finishing_tactics_test.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_choose.glob
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/it_holds_that_test.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/goal_to_hint.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_apply.vo
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/such_that_test.glob
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_auxiliary_test.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/simplify.vo
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/take_test.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/induction.vo
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_claims.vo
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/define.vo
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_know.glob
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/automation_databases/decidability_db.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/it_holds_that_test.glob
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_because.glob
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/claims.vo
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_choose_such_that.glob
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/it_suffices_to_show_test.glob
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/apply.vo
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/reverse_engineer/auto_hintdb_arg.vo
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_show_both_directions.vo
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/proof_finishing_tactics.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_define.vo
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_simplify.vo
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/write_using_test.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/forward_reasoning_aux.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/it_suffices_to_show_test.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_show_both_statements.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/choose.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_set_search_depth.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_know.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/unfold_test.glob
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/write_as.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_sets_tactics/test_sets_automation_tactics.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/we_need_to_show.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/AllTactics.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_auxiliary_test.glob
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/string_auxiliary_test.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/we_know.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/because.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/such_that_test.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/unfold.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/reverse_engineer/auto_hintdb_arg.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/rewrite_inequalities.glob
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_show_both_directions.glob
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_choose_such_that.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_either.glob
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/unfold_test.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/contradiction_tactics/basic_contradiction.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/we_need_to_show_test.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/either.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/we_show_both_directions.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_choose.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/AllTactics.glob
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_define.glob
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/notations/set_notations.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_set_search_depth.glob
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/write_as_test.glob
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_set_intuition.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/goal_to_hint_test.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/choose_such_that.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/notations/set_notations.glob
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/we_need_to_show_test.glob
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/All.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_because.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_apply.glob
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/write_as_test.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_show_both_directions.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_apply.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/induction.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_set_intuition.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_simplify.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/goal_to_hint_test.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_either.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_contradiction_tactics/test_basic_contradiction.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_contradiction_tactics/test_basic_contradiction.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/define.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_define.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/definitions/set_definitions.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/apply.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_claims.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/definitions/set_definitions.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_simplify.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_induction.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_intuition/Disabled.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_intuition/Enabled.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/RealsAndIntegers.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/EnableWildcard.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/Multiplication.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/DisableWildcard.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/AbsoluteValue.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/Exponential.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/SquareRoot.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/PlusMinus.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_1.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_3.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_5.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_2.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_4.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/Sets.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/Additional.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/ZeroOne.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/Other.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/reals.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/claims.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/forward_reasoning_aux.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_induction.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/sets_tactics/sets_automation_tactics.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/simplify.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_claims.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/we_conclude_that.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/All.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/either.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/contradiction_tactics/basic_contradiction.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/assume.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test_auxiliary.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/auxiliary.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/choose.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/waterprove/waterprove.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/rewrite_using.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/goal_to_hint.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/selected_databases.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/it_suffices_to_show.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/it_holds_that.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/write_as.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/we_show_both_statements.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/proof_finishing_tactics.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/we_know.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/write_using.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/string_auxiliary_test.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/we_show_both_directions.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/we_need_to_show.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/take.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_intuition/Disabled.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_intuition/Enabled.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/test/reverse_engineer/auto_hintdb_arg.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/unfold.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/DisableWildcard.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/EnableWildcard.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/RealsAndIntegers.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/Multiplication.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/AbsoluteValue.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/Exponential.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/SquareRoot.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/PlusMinus.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/Additional.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_4.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_5.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_1.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_3.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_2.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/ZeroOne.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/claims.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/Sets.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/Other.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/load_database/reals.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/define.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/choose_such_that.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/string_auxiliary.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/induction.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/simplify.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/apply.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/Waterproof/tactics/because.glob

Uninstall

Command
opam remove -y coq-waterproof.1.0.0
Return code
0
Missing removes
none
Wrong removes
none