« Up

tactician 1.0~beta1+8.13 1 m 0 s 🏆

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              4           Virtual package relying on a GMP lib system installation
coq                   8.13.0      Formal proof management system
num                   1.4         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml                 4.14.0      The OCaml compiler (virtual package)
ocaml-base-compiler   4.14.0      Official release 4.14.0
ocaml-config          2           OCaml Switch Configuration
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special options enabled
ocamlfind             1.9.3       A library manager for OCaml
zarith                1.12        Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
name: "coq-tactician"
synopsis: "Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq"
description: """
  Tactician is a tactic learner and prover for the Coq Proof Assistant.
  The system will help users make tactical proof decisions while they retain
  control over the general proof strategy. To this end, Tactician will learn
  from previously written tactic scripts, and either gives the user suggestions
  about the next tactic to be executed or altogether takes over the burden of
  proof synthesis. Tactician's goal is to provide the user with a seamless,
  interactive, and intuitive experience together with strong, adaptive proof
  automation.
"""
homepage: "https://coq-tactician.github.io"
dev-repo: "git+https://github.com/coq-tactician/coq-tactician"
bug-reports: "https://github.com/coq-tactician/coq-tactician/issues"
maintainer: "Lasse Blaauwbroek <lasse@blaauwbroek.eu>"
authors: "Lasse Blaauwbroek <lasse@blaauwbroek.eu"
depends: [
  "ocaml" {>= "4.08"}
  "dune" {>= "2.5"}
  "opam-client" {>= "2.1.0~beta2"}
  "cmdliner"
  "coq" {>= "8.13" & < "8.14~"}
  "coq-tactician-dummy"
]
depexts: ["git"]
build: [
  ["dune" "build" "--release" "-j" jobs]
]
post-messages: ["
--- Tactician was successfully installed ---
In order to enable Tactician, you should run
tactician enable
" {success}]
url {
  src: "https://github.com/coq-tactician/coq-tactician/archive/1.0-beta1-8.13.tar.gz"
}
tags: [
  "keyword:tactic-learning"
  "keyword:machine-learning"
  "keyword:automation"
  "keyword:proof-synthesis"
  "category:Miscellaneous/Coq Extensions"
  "logpath:Tactician"
]

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-tactician.1.0~beta1+8.13 coq.8.13.0
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-tactician.1.0~beta1+8.13 coq.8.13.0
Return code
0
Duration
8 m 0 s

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-tactician.1.0~beta1+8.13 coq.8.13.0
Return code
0
Duration
1 m 0 s

Installation size

Total: 24 M

  • 14 M ../ocaml-base-compiler.4.14.0/bin/tactician
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cma
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.a
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmxs
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Tactician/tactician_ltac1_record_plugin.cmxs
  • 944 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Map_ssr_witnesses.cmt
  • 758 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmt
  • 435 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cma
  • 434 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Ltacrecord.cmt
  • 235 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_witnesses.cmt
  • 175 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_annotate.cmt
  • 166 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmxs
  • 166 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Tactician/tactician_ssreflect_plugin.cmxs
  • 158 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__G_ltac1_record.cmt
  • 156 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.a
  • 129 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Cook_tacexpr.cmt
  • 116 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_subst_learner.cmt
  • 109 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmxa
  • 109 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitute.cmt
  • 109 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner_internal.cmt
  • 83 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Learner_helper.cmt
  • 80 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Sexpr.cmt
  • 76 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmti
  • 70 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_normalize.cmt
  • 54 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Known_ssr_witnesses.cmt
  • 52 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmti
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/map_all_the_things.ml
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Known_witnesses.cmt
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Gendischarge.cmt
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/ltacrecord.ml
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/g_ltac1_record.ml
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmxs
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Tactician/tactician_ltac1_tactics_plugin.cmxs
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin__G_ltac1_tactics.cmt
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Diagonal_iterative_search.cmt
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Tactician/Ltac1/Record.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Ltacrecord.cmi
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner_internal.cmi
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactician_util.cmt
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Mapping_helpers.cmt
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitute.cmi
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmi
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Ltacrecord.cmx
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Timeouttac.cmt
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmt
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmi
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy_internal.cmt
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/map_ssr_witnesses.ml
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_annotate.cmi
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cma
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_normalize.cmi
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Map_ssr_witnesses.cmi
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitute.cmx
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner_internal.cmx
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmt
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/dune-package
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.a
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_normalize.cmx
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmx
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmxa
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmti
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactic_annotate.ml
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/map_all_the_witnesses.ml
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Map_ssr_witnesses.cmx
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_annotate.cmx
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmx
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmt
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__G_ltac1_record.cmx
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__G_ltac1_record.cmi
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Learner_helper.cmx
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/cook_tacexpr.ml
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Learner_helper.cmi
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Cook_tacexpr.cmi
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_subst_learner.cmx
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Gendischarge.cmi
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmxa
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/naiveknn_subst_learner.ml
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin__G_ltac1_tactics.cmx
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin__G_ltac1_tactics.cmi
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_witnesses.cmx
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Mapping_helpers.cmi
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Cook_tacexpr.cmx
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Known_ssr_witnesses.cmx
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Sexpr.cmx
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Known_witnesses.cmi
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Known_ssr_witnesses.cmi
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Known_witnesses.cmx
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_witnesses.cmi
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_subst_learner.cmi
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Mapping_helpers.cmx
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/learner_helper.ml
  • 6 K ../ocaml-base-compiler.4.14.0/share/coq-tactician/coq-hott.8.11.patch
  • 6 K ../ocaml-base-compiler.4.14.0/share/coq-tactician/coq-hott.patch
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactic_learner_internal.ml
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Sexpr.cmi
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/sexpr.ml
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/map_all_the_things.mli
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy_internal.cmx
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy_internal.cmi
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Diagonal_iterative_search.cmi
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Gendischarge.cmx
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactician_util.cmi
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Diagonal_iterative_search.cmx
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmx
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmi
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmt
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmi
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Timeouttac.cmi
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Timeouttac.cmx
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.ml
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmt
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactic_substitute.ml
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactic_learner.mli
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/known_ssr_witnesses.ml
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactician_util.cmx
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/diagonal_iterative_search.ml
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/g_ltac1_tactics.ml
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactic_normalize.ml
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/gendischarge.ml
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/known_witnesses.ml
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Tactician/Ltac1/Record.v
  • 2 K ../ocaml-base-compiler.4.14.0/man/man1/tactician-enable.1
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Tactician/Ltac1/Tactics.vo
  • 2 K ../ocaml-base-compiler.4.14.0/man/man1/tactician.1
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/opam
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/timeouttac.ml
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/META
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmx
  • 1 K ../ocaml-base-compiler.4.14.0/man/man1/tactician-recompile.1
  • 1 K ../ocaml-base-compiler.4.14.0/man/man1/tactician-eject.1
  • 1 K ../ocaml-base-compiler.4.14.0/man/man1/tactician-inject.1
  • 1 K ../ocaml-base-compiler.4.14.0/man/man1/tactician-disable.1
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_util.ml
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Tactician/Ltac1.vo
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Tactician/Ltac1/Tactics.v
  • 1 K ../ocaml-base-compiler.4.14.0/bin/tactician-patch
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactic_learner.ml
  • 1 K ../ocaml-base-compiler.4.14.0/doc/coq-tactician/LICENSE.md
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmi
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/search_strategy_internal.ml
  • 1 K ../ocaml-base-compiler.4.14.0/bin/with-tactician
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/mapping_helpers.ml
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/search_strategy.mli
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmi
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/search_strategy.ml
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.ml
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmx
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmx
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.ml
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Tactician/Ltac1.v
  • 0 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/coqc.real

Uninstall 🧹

Command
opam remove -y coq-tactician.1.0~beta1+8.13
Return code
0
Missing removes
none
Wrong removes
none

Sources are on GitHub © Guillaume Claret 🐣