# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
coq 8.12.1 Formal proof management system
num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.10.2 The OCaml compiler (virtual package)
ocaml-base-compiler 4.10.2 Official release 4.10.2
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.6 A library manager for OCaml
# 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>"]
license: "MIT"
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"}
"cmdliner" {>= "1.1.0"}
"coq" {>= "8.12" & < "8.13~"}
"conf-git"
"bos" {>= "0.2.1"}
"coq-tactician-dummy" {= "1.0~beta2+8.11" & 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: "https://github.com/coq-tactician/coq-tactician/archive/1.0-beta2.1-8.12.tar.gz"
checksum: "sha512=479eda00e57b3107e11e7bb0fcd3fab45d4f499ef0b83520f22fef507f5c8771dd6775a5e26799a99c37e9b29e665d3d7cbe46ac2f854a3969167f8174c2155f"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-tactician.1.0~beta2.1+8.12 coq.8.12.1Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-tactician.1.0~beta2.1+8.12 coq.8.12.1opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-tactician.1.0~beta2.1+8.12 coq.8.12.1Total: 35 M
../ocaml-base-compiler.4.10.2/bin/tactician../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cma../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.a../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmxs../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Tactician/tactician_ltac1_record_plugin.cmxs../ocaml-base-compiler.4.10.2/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Map_ssr_witnesses.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Ltacrecord.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cma../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Monad_util.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_witnesses.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Features.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmxa../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_one_variable.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_sexpr.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__G_ltac1_record.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_annotate.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmxs../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Tactician/tactician_ssreflect_plugin.cmxs../ocaml-base-compiler.4.10.2/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.a../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Lshf_learner.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_subst_learner.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner_internal.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Offline_evaluation_simulator_learner.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitute.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_abstract.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_learner.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Inline_private_constants.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Learner_helper.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmti../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_normalize.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Sexpr.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactician_util.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Cook_tacexpr.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Find_tactic_syntax.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitution_check_learner.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Extreme_tactic_normalize.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Trivial_learners.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmti../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Benchmark.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Timeouttac.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin__G_ltac1_tactics.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Diagonal_iterative_search.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/map_all_the_things.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/ltacrecord.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmxs../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Tactician/tactician_ltac1_tactics_plugin.cmxs../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Dijkstra_iterative_search.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/g_ltac1_record.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Monad_util.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_one_variable.cmi../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Tactician/Ltac1/Record.vo../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Mapping_helpers.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cma../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_abstract.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Ltacrecord.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitute.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner_internal.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/features.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy_internal.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/dune-package../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.a../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_sexpr.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Learner_helper.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Ltacrecord.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmti../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Cook_tacexpr.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Find_tactic_syntax.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/ssreflect-plugin/map_ssr_witnesses.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_normalize.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Features.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Inline_private_constants.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_one_variable.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Map_ssr_witnesses.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Extreme_tactic_normalize.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_annotate.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner_internal.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_abstract.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_sexpr.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitute.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_normalize.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/map_all_the_witnesses.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactic_annotate.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Lshf_learner.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Extreme_tactic_normalize.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Inline_private_constants.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Cook_tacexpr.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Find_tactic_syntax.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Features.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_learner.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_subst_learner.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Lshf_learner.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_learner.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Offline_evaluation_simulator_learner.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__G_ltac1_record.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/monad_util.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Learner_helper.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Map_ssr_witnesses.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__G_ltac1_record.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_subst_learner.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Trivial_learners.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Benchmark.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Monad_util.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmxa../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Offline_evaluation_simulator_learner.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin__G_ltac1_tactics.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_annotate.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Benchmark.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin__G_ltac1_tactics.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactic_sexpr.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitution_check_learner.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitution_check_learner.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactic_learner_internal.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/offline_evaluation_simulator_learner.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactic_one_variable.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_witnesses.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Mapping_helpers.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactician_util.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Trivial_learners.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_witnesses.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/naiveknn_subst_learner.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmxa../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/map_all_the_things.mli../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Mapping_helpers.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactician_util.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Sexpr.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/lshf_learner.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Diagonal_iterative_search.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Dijkstra_iterative_search.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Sexpr.cmi../ocaml-base-compiler.4.10.2/doc/coq-tactician/README.md../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Diagonal_iterative_search.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Dijkstra_iterative_search.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_util.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/sexpr.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/tactics-plugin/g_ltac1_tactics.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/inline_private_constants.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Timeouttac.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/timeouttac.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy_internal.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Timeouttac.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/naiveknn_learner.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactic_substitution_check_learner.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/benchmark.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy_internal.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/learner_helper.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/trivial_learners.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/diagonal_iterative_search.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactic_learner.mli../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Tactician/Ltac1/Record.v../ocaml-base-compiler.4.10.2/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmt../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/dijkstra_iterative_search.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactic_normalize.ml../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Tactician/Ltac1/Tactics.vo../ocaml-base-compiler.4.10.2/man/man1/tactician.1../ocaml-base-compiler.4.10.2/man/man1/tactician-enable.1../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/opam../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/cook_tacexpr.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactic_abstract.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/find_tactic_syntax.ml../ocaml-base-compiler.4.10.2/man/man1/tactician-recompile.1../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactic_substitute.ml../ocaml-base-compiler.4.10.2/man/man1/tactician-eject.1../ocaml-base-compiler.4.10.2/man/man1/tactician-inject.1../ocaml-base-compiler.4.10.2/lib/coq-tactician/META../ocaml-base-compiler.4.10.2/man/man1/tactician-disable.1../ocaml-base-compiler.4.10.2/doc/coq-tactician/LICENSE.md../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Tactician/Ltac1/Tactics.v../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/extreme_tactic_normalize.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/tactic_learner.ml../ocaml-base-compiler.4.10.2/share/coq-tactician/coq-hott.patch../ocaml-base-compiler.4.10.2/share/coq-tactician/coq-hott.8.14.patch../ocaml-base-compiler.4.10.2/share/coq-tactician/coq-hott.8.15.patch../ocaml-base-compiler.4.10.2/share/coq-tactician/coq-hott.8.11.patch../ocaml-base-compiler.4.10.2/share/coq-tactician/coq-hott.8.10.patch../ocaml-base-compiler.4.10.2/share/coq-tactician/coq-hott.8.13.patch../ocaml-base-compiler.4.10.2/share/coq-tactician/coq-hott.8.12.patch../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Tactician/Ltac1.vo../ocaml-base-compiler.4.10.2/lib/coq-tactician/tactician-patch../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/search_strategy_internal.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/search_strategy.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/mapping_helpers.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/record-plugin/search_strategy.mli../ocaml-base-compiler.4.10.2/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmi../ocaml-base-compiler.4.10.2/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmx../ocaml-base-compiler.4.10.2/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.ml../ocaml-base-compiler.4.10.2/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.ml../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Tactician/Ltac1.v../ocaml-base-compiler.4.10.2/etc/coq-tactician/injection-flags../ocaml-base-compiler.4.10.2/lib/coq-tactician/coqide.real../ocaml-base-compiler.4.10.2/lib/coq-tactician/coqc.real../ocaml-base-compiler.4.10.2/lib/coq-tactician/coqidetop.real../ocaml-base-compiler.4.10.2/lib/coq-tactician/coqtop.real../ocaml-base-compiler.4.10.2/share/coq-tactician/plugins/coq-tactician/injection-flagsopam remove -y coq-tactician.1.0~beta2.1+8.12