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. 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.