package coq-tactician-stdlib

*** 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. The new .vo files are equivalent to the originals, except that they also contain Tactician's tactic databases. After installation of this package, all other Coq developments that are installed will also need to be recompiled. The 'tactician recompile' command line utility can help with this. Upon removal of this package, the original files will be placed back.