coq-toolbox

A series of auxiliary tactics for Coq. These tactics won't change the proof environment but just give internal information of Coq. These tactics are very useful when you're developing an ML plugin. Up to now, these tactics are available: - print_term: print the CiC term - print_term_constant: print the target term of CONST term - print_goal: print the CiC term of goal - print_hyps: print the CiC terms of hypotheses

opam install coq-toolbox.0.9.0
homepage
https://github.com/hengruoz/coq-toolbox
license
MIT
bugs tracker
https://github.com/hengruoz/coq-toolbox/issues
dependencies
coq (>= 8.5.2 & < 8.6.0)
source
https://github.com/hengruoz/coq-toolbox/archive/0.9.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-toolbox/coq-toolbox.0.9.0