index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
btauto
/
Btauto.v
blob: d3331ccf8939d3b02f1ed44f49880b31122669d7 (
plain
)
1
2
3
Require
Import
Algebra
Reflect
.
Declare
ML
Module
"btauto_plugin"
.
