index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
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".