package coq-tactician-stdlib

  1. Overview
  2. Homepage
Recompiles Coq's standard libary with Tactician's instrumentation loaded

Install

Dune Dependency

Authors

Maintainers

Sources

1.0-beta1-8.12.tar.gz
sha512=a5a24c47eb8b28663a790cf3a935d7ccc59a856777d659be5b9ad2ef17a793c10a5c824a46fb52627eaf09eb07f553f4e0c16a58ffdec7eb53a9b5908e146f41

Description

*** WARNING *** This package will overwrite Coq's standard library files.

This package recompiles Coq's standard library with Tactician's (coq-tactician) instrumentation loaded such that Tactician can learn from the library. When you install this package, the current .vo files of the standard library are backed in the folder user-contrib/Tactician/stdlib-backup. Then exactly the same .vo files are installed, except that they also contain Tactician's tactic databases. Upon removal of this package, the original files will be placed back.

Dependencies (2)

  1. coq-tactician
  2. coq >= "8.12" & < "8.13~"

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover