index
:
coq-mathcomp
master
Library of mathematical components formalized in Coq
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
mathcomp
/
ssreflect
/
plugin
Age
Commit message (
Expand
)
Author
2015-12-04
update license banner in .ml files
Enrico Tassi
2015-12-03
Removing the only use of globTacticIn.
Pierre-Marie Pédrot
2015-12-03
fix compilation on trunk (thanks PMP)
Enrico Tassi
2015-12-03
fix: autogen + abstract variables clash
Enrico Tassi
2015-12-03
fix: elim/v handles eliminator from Derive Inversion (issue #2)
Enrico Tassi
2015-12-03
Add commands to trace the matching algorithm
Enrico Tassi
2015-12-03
fix: Hint View is not a Query
Enrico Tassi
2015-09-27
fix compilation on trunk
Enrico Tassi
2015-09-24
Fix compilation on 8.5
Enrico Tassi
2015-08-24
Compare pattern heads (constants) up to "univs"
Enrico Tassi
2015-07-30
fix trunk compilation
Enrico Tassi
2015-07-22
blind patch by Enrico
Cyril Cohen
2015-07-21
keeping track of the changes for trunk (import from svn)
Cyril Cohen
2015-07-18
update to preserve backward compatibility with v8.4
Cyril Cohen
2015-07-17
Updating files + reorganizing everything
Cyril Cohen
2015-04-09
support for camlp4
Enrico Tassi
2015-04-09
Forward compatibility with "From X Require Y."
Enrico Tassi
2015-04-02
support both coq.8.5beta1 and coq.8.5.dev
Enrico Tassi
2015-04-02
plugin that compiles with 8.5
Enrico Tassi
2015-03-09
Initial commit
Enrico Tassi