# 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 dev Formal proof management system
dune 3.0.3 Fast, portable, and opinionated build system
ocaml 4.08.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.08.1 Official release 4.08.1
ocaml-config 1 OCaml Switch Configuration
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"
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."""
maintainer: ["Lasse Blaauwbroek <lasse@blaauwbroek.eu>"]
authors: ["Lasse Blaauwbroek <lasse@blaauwbroek.eu>"]
homepage: "https://coq-tactician.github.io"
bug-reports: "https://github.com/coq-tactician/coq-tactician/issues"
depends: [
"ocaml" {>= "4.08"}
"dune" {>= "2.8"}
"dune-site" {>= "2.9.1"}
"opam-client" {>= "2.1.0~beta2"}
"cmdliner"
"coq" {= "dev"}
"conf-git"
"bos" {>= "0.2.1"}
"coq-tactician-dummy" {= "dev" & with-test}
"odoc" {with-doc}
]
build: [
["dune" "subst"] {dev}
[
"dune"
"build"
"-p"
name
"-j"
jobs
"@install"
"@runtest" {with-test}
"@doc" {with-doc}
]
]
dev-repo: "git+https://github.com/coq-tactician/coq-tactician.git"
post-messages: ["
--- Tactician was successfully installed ---
In order to enable Tactician, you should run
tactician enable
" {success}]
tags: [
"keyword:tactic-learning"
"keyword:machine-learning"
"keyword:automation"
"keyword:proof-synthesis"
"category:Miscellaneous/Coq Extensions"
"logpath:Tactician"
]
substs: [
"coq-shim/tactician-patch"
"coq-shim/tactician.ml"
]
url {
src: "git+https://github.com/coq-tactician/coq-tactician.git#coqdev"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-tactician.dev coq.devDry 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-tactician.dev coq.devopam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y coq-tactician.dev coq.devTotal: 35 M
../ocaml-base-compiler.4.08.1/bin/tactician../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cma../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.a../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmxs../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Tactician/tactician_ltac1_record_plugin.cmxs../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Map_ssr_witnesses.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Ltacrecord.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cma../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Features.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_witnesses.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactician_util.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_sexpr.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_annotate.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmxs../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Tactician/tactician_ssreflect_plugin.cmxs../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.a../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__G_ltac1_record.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Cook_tacexpr.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmxa../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_subst_learner.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Lshf_learner.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner_internal.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Offline_evaluation_simulator_learner.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitute.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_abstract.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_learner.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Learner_helper.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Sexpr.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Inline_private_constants.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmti../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Knn.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_normalize.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Find_tactic_syntax.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Known_ssr_witnesses.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Trivial_learners.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmti../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Known_witnesses.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/map_all_the_things.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Gendischarge.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/ltacrecord.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin__G_ltac1_tactics.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Diagonal_iterative_search.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/g_ltac1_record.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmxs../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Tactician/tactician_ltac1_tactics_plugin.cmxs../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Tactician/Ltac1/Record.vo../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Mapping_helpers.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Timeouttac.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Ltacrecord.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/features.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy_internal.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner_internal.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_abstract.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cma../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitute.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactician_util.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmti../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Ltacrecord.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Learner_helper.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_sexpr.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/dune-package../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/map_ssr_witnesses.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Map_ssr_witnesses.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Find_tactic_syntax.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Features.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_normalize.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Inline_private_constants.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactician_util.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmxa../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.a../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_annotate.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactic_annotate.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_abstract.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner_internal.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitute.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_sexpr.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/map_all_the_witnesses.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_subst_learner.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Lshf_learner.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_normalize.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_util.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Inline_private_constants.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Find_tactic_syntax.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__G_ltac1_record.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Map_ssr_witnesses.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_subst_learner.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Features.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_learner.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Offline_evaluation_simulator_learner.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__G_ltac1_record.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactic_sexpr.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Lshf_learner.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_learner.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/cook_tacexpr.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Learner_helper.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_witnesses.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Offline_evaluation_simulator_learner.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Known_ssr_witnesses.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Known_ssr_witnesses.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmxa../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin__G_ltac1_tactics.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Known_witnesses.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_witnesses.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Trivial_learners.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Known_witnesses.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Gendischarge.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin__G_ltac1_tactics.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/offline_evaluation_simulator_learner.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactic_learner_internal.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Knn.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_annotate.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/naiveknn_subst_learner.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Cook_tacexpr.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/knn.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Sexpr.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/lshf_learner.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/map_all_the_things.mli../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Cook_tacexpr.cmx../ocaml-base-compiler.4.08.1/share/coq-tactician/coq-hott.8.11.patch../ocaml-base-compiler.4.08.1/share/coq-tactician/coq-hott.patch../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Mapping_helpers.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Sexpr.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/sexpr.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Trivial_learners.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Diagonal_iterative_search.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Mapping_helpers.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Diagonal_iterative_search.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy_internal.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy_internal.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/inline_private_constants.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/naiveknn_learner.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/learner_helper.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Gendischarge.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/trivial_learners.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Timeouttac.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Timeouttac.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmt../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Tactician/Ltac1/Record.v../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactic_learner.mli../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactic_abstract.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/known_ssr_witnesses.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactic_substitute.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactic_normalize.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/diagonal_iterative_search.ml../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Tactician/Ltac1/Tactics.vo../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/g_ltac1_tactics.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/gendischarge.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/opam../ocaml-base-compiler.4.08.1/man/man1/tactician.1../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/find_tactic_syntax.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/known_witnesses.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmx../ocaml-base-compiler.4.08.1/man/man1/tactician-enable.1../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Knn.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/timeouttac.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/META../ocaml-base-compiler.4.08.1/man/man1/tactician-recompile.1../ocaml-base-compiler.4.08.1/man/man1/tactician-eject.1../ocaml-base-compiler.4.08.1/man/man1/tactician-inject.1../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactic_learner.ml../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Tactician/Ltac1/Tactics.v../ocaml-base-compiler.4.08.1/man/man1/tactician-disable.1../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Tactician/Ltac1.vo../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactician-patch../ocaml-base-compiler.4.08.1/doc/coq-tactician/LICENSE.md../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/search_strategy_internal.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/mapping_helpers.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/search_strategy.mli../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/search_strategy.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.ml../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Tactician/Ltac1.v../ocaml-base-compiler.4.08.1/etc/coq-tactician/injection-flags../ocaml-base-compiler.4.08.1/lib/coq-tactician/coqc.real../ocaml-base-compiler.4.08.1/lib/coq-tactician/coqtop.real../ocaml-base-compiler.4.08.1/share/coq-tactician/plugins/coq-tactician/injection-flagsopam remove -y coq-tactician.dev