« Up

waterproof 1.1.2 3 m 0 s 🏆

Context

# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-num            base        Num library distributed with the OCaml compiler
base-threads        base
base-unix           base
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                 0           The Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.05.0      The OCaml compiler (virtual package)
ocaml-base-compiler 4.05.0      Official 4.05.0 release
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.9.5       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: [
  "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"
]

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-waterproof.1.1.2 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.1.2 coq.8.13.1
Return code
0
Duration
1 m 0 s

Install 🚀

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

Installation size

Total: 5 M

  • 141 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/sup_and_inf_new_definitions.glob
  • 95 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/sequences.glob
  • 95 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_databases/test_waterproof_integers_database.vo
  • 89 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_databases/test_reals_database.vo
  • 81 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/databases.vo
  • 80 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/limsup_liminf_bolzano.glob
  • 78 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/sequences.vo
  • 78 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_manipulate_negation.glob
  • 73 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/sup_and_inf.glob
  • 69 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/subsequences.glob
  • 68 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/sup_and_inf_new_definitions.vo
  • 68 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_goal_wrappers.vo
  • 68 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_manipulate_negation.vo
  • 63 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/limsup_liminf_bolzano.vo
  • 63 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_inequality_chains.vo
  • 62 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/subsequences.vo
  • 62 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/definitions/inequality_chains.vo
  • 60 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/waterprove/manipulate_negation.vo
  • 54 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/subsequences_metric.vo
  • 54 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/sup_and_inf.vo
  • 50 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/series.vo
  • 48 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_databases/test_waterproof_integers_database.glob
  • 45 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/waterprove/manipulate_negation.glob
  • 44 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/we_conclude_that_test.vo
  • 44 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_databases/test_reals_database.glob
  • 42 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_sets_tactics/test_sets_automation_tactics.vo
  • 42 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_either.vo
  • 41 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/either.vo
  • 41 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_load_database.vo
  • 40 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/metric_spaces.vo
  • 40 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_shield_automation.vo
  • 39 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/it_holds_that_test.vo
  • 39 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_set_definitions.vo
  • 38 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/databases.glob
  • 38 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/notations/notations.vo
  • 37 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/sequential_accumulation_points.vo
  • 37 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/sets_tactics/sets_automation_tactics.vo
  • 37 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/subsequences_metric.glob
  • 35 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_contradiction.vo
  • 35 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/we_conclude_that.vo
  • 35 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_because.vo
  • 35 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/because.vo
  • 34 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_goal_wrappers.glob
  • 34 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_choose_such_that.vo
  • 34 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/AllTactics.vo
  • 34 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/it_suffices_to_show_test.vo
  • 33 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/AllConstructiveTactics.vo
  • 33 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_simplify_chains.vo
  • 33 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/take_test.vo
  • 32 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/it_holds_that.vo
  • 32 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/it_suffices_to_show.vo
  • 32 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/selected_databases.vo
  • 32 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/waterprove/automation_subroutine.vo
  • 32 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/waterprove/waterprove.vo
  • 31 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/notations/set_notations.vo
  • 31 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_set_search_depth.vo
  • 31 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/All.vo
  • 31 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/simplify_chains.vo
  • 31 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/forward_reasoning_aux.vo
  • 31 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_set_intuition.vo
  • 31 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/series.glob
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_shield_automation.glob
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/RealsAndIntegers.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/RealNumbers.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/sequences_metric.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/DisableWildcard.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/EnableWildcard.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_intuition/Disabled.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_intuition/Enabled.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Integers.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/sup_and_inf_new_definitions.v
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/ConstructiveLogic.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Multiplication.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/ClassicalLogic.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/AbsoluteValue.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Exponential.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Additional.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Firstorder.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/SquareRoot.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Intuition.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/PlusMinus.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/ZeroOne.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Subsets.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Sets.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/definitions/set_definitions.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_2.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_4.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_1.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_5.vo
  • 30 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_3.vo
  • 21 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/databases.v
  • 19 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_load_database.glob
  • 19 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_either.glob
  • 18 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/sequences.v
  • 18 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/goal_wrappers.vo
  • 16 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_inequality_chains.glob
  • 16 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/sup_and_inf.v
  • 16 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/goal_wrappers.glob
  • 16 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/definitions/inequality_chains.glob
  • 15 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/limsup_liminf_bolzano.v
  • 15 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_choose_such_that.glob
  • 14 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/subsequences.v
  • 14 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_because.glob
  • 14 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_load_database.v
  • 13 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/unfold_test.vo
  • 13 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/waterprove/manipulate_negation.v
  • 13 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/take_test.glob
  • 12 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/assume_test.glob
  • 12 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/goal_to_hint_test.vo
  • 11 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/contradiction.vo
  • 11 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/sequential_accumulation_points.glob
  • 11 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/metric_spaces.glob
  • 10 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/either.glob
  • 9 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_show_both_statements.vo
  • 9 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_show_both_statements.glob
  • 9 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_induction.vo
  • 9 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/definitions/inequality_chains.v
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/unfold.vo
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test_auxiliary.v
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/we_need_to_show_test.vo
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/auxiliary.v
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/subsequences_metric.v
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/induction.vo
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/such_that_test.vo
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/choose_such_that.vo
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/we_conclude_that.v
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/assume_test.vo
  • 8 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/auxiliary.vo
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/we_show_both_statements.vo
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/we_conclude_that_test.glob
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/notations/notations.glob
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/assume.vo
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_auxiliary_test.vo
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/selected_databases.v
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test_auxiliary.vo
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/string_auxiliary.v
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/either.v
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/it_suffices_to_show.v
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_choose.vo
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/assume.v
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/series.v
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/waterprove/automation_subroutine.v
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/we_need_to_show.vo
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_sets_tactics/test_sets_automation_tactics.glob
  • 7 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/goal_to_hint.vo
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/take.vo
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_set_definitions.glob
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/unfold_test.glob
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/unfold.v
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_manipulate_negation.v
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/we_show_both_statements.v
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/notations/notations.v
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/goal_wrappers.v
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/we_conclude_that_test.v
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/choose.vo
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/take.v
  • 6 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/we_need_to_show.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/because.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_show_both_directions.vo
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/goal_to_hint.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/we_show_both_directions.vo
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/string_auxiliary_test.vo
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/string_auxiliary.vo
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/sets_tactics/sets_automation_tactics.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/it_holds_that_test.glob
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_shield_automation.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/take_test.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/it_holds_that.v
  • 5 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_define.vo
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/define.vo
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/waterprove/waterprove.v
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_claims.vo
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/it_suffices_to_show_test.glob
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/claims.vo
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/choose_such_that.v
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/induction.v
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_choose.glob
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/it_holds_that_test.v
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/assume_test.v
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/sequences_metric.glob
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_auxiliary_test.v
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/such_that_test.glob
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_either.v
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_because.v
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/reverse_engineer/auto_hintdb_arg.vo
  • 4 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/it_suffices_to_show_test.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_choose_such_that.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_set_definitions.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/goal_to_hint_test.glob
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_show_both_directions.glob
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_show_both_statements.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/choose.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/forward_reasoning_aux.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/unfold_test.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_sets_tactics/test_sets_automation_tactics.v
  • 3 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_set_search_depth.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_auxiliary_test.glob
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/sequential_accumulation_points.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/goal_to_hint_test.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/metric_spaces.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/string_auxiliary_test.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_induction.glob
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/we_need_to_show_test.glob
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/such_that_test.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/we_show_both_directions.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/we_need_to_show_test.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/reverse_engineer/auto_hintdb_arg.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/AllTactics.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_define.glob
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_goal_wrappers.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/AllConstructiveTactics.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_contradiction.glob
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_choose.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/contradiction.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/simplify_chains.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_set_search_depth.glob
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_induction.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/notations/set_notations.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_set_intuition.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_databases/test_waterproof_integers_database.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_we_show_both_directions.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_simplify_chains.glob
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/All.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_contradiction.v
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/notations/set_notations.glob
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_claims.glob
  • 2 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/define.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_simplify_chains.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_inequality_chains.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_claims.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/RealsAndIntegers.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/claims.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/RealNumbers.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_set_intuition.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/AllTactics.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/definitions/set_definitions.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_databases/test_reals_database.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/test_tactics/test_forward_reasoning/test_define.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Integers.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/AllConstructiveTactics.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/sets_tactics/sets_automation_tactics.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/we_conclude_that.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/EnableWildcard.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/DisableWildcard.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_intuition/Disabled.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_intuition/Enabled.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/ClassicalLogic.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Multiplication.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/AbsoluteValue.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Exponential.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/ConstructiveLogic.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/SquareRoot.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Additional.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/PlusMinus.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Sets.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_1.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_3.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_5.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_2.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_4.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/ZeroOne.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Firstorder.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Intuition.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Subsets.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/induction.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/definitions/set_definitions.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/goal_to_hint.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/unfold.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/All.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/auxiliary.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/theory/analysis/sequences_metric.v
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/we_need_to_show.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/waterprove/waterprove.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test_auxiliary.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/we_show_both_statements.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/choose.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/simplify_chains.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/choose_such_that.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/assume.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/it_holds_that.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/because.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/forward_reasoning_aux.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/we_show_both_directions.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/it_suffices_to_show.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/string_auxiliary_test.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/waterprove/automation_subroutine.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/take.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/selected_databases.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/define.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/contradiction.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/tactics/forward_reasoning/claims.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_intuition/Disabled.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_intuition/Enabled.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/test/reverse_engineer/auto_hintdb_arg.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/DisableWildcard.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/EnableWildcard.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/ConstructiveLogic.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/RealsAndIntegers.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/ClassicalLogic.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Multiplication.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/AbsoluteValue.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Exponential.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/SquareRoot.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Additional.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/RealNumbers.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/PlusMinus.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Firstorder.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_4.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_5.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_1.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_3.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/set_search_depth/To_2.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Intuition.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Integers.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/ZeroOne.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Subsets.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/load_database/Sets.glob
  • 1 K ../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Waterproof/string_auxiliary.glob

Uninstall 🧹

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