index
:
debian-coq
master
pristine-tar
upstream
Debian packaging for Coq
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".