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
/
trunk
Age
Commit message (
Expand
)
Author
2016-05-02
Fixing compilation after the merge of ML-tactic-notation branch.
Pierre-Marie Pédrot
2016-03-27
Fixing ML compilation.
Pierre-Marie Pédrot
2016-03-03
[search] Use msg_info to notify search results.
Emilio Jesus Gallego Arias
2016-03-02
fix compilation of ssrmatching in trunk
Enrico Tassi
2016-02-25
fix compilation
Enrico Tassi
2016-02-25
ssrpattern: compose nicely with Tactic Notation
Enrico Tassi
2016-02-22
Guard "catch all" exception handler using Errors.noncritical
Enrico Tassi
2016-02-22
rewrite: matching do not instantiate goal evars
Enrico Tassi
2016-02-18
typo in error message
thery
2016-02-15
Removing compatibility layers.
Pierre-Marie Pédrot
2016-02-15
Fixing ML compilation with trunk.
Pierre-Marie Pédrot
2016-02-03
Register flag "SsrHave NoTCResolution" in the Summary (fix #6)
Enrico Tassi
2016-02-03
resolve type classes under the correct set of univs (fix #22)
Enrico Tassi
2016-02-02
Do not hide critical errors with a blind catch all (fix #19)
Enrico Tassi
2016-02-02
fix debug print
Enrico Tassi
2016-02-02
Explicit error message if rewrite fails due to TC inference (fix #21)
Enrico Tassi
2016-02-01
compilation on trunk fixed
Enrico Tassi
2016-01-31
Partially fixing ML compilation on trunk.
Pierre-Marie Pédrot
2016-01-31
half-repair compilation on trunk
Enrico Tassi
2016-01-12
Move bullet initialization to ssreflect.v
Robbert Krebbers
2016-01-08
fix version number in initialization message
Enrico Tassi
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-07-22
blind patch by Enrico
Cyril Cohen
2015-07-21
keeping track of the changes for trunk (import from svn)
Cyril Cohen
2015-04-02
plugin that compiles with 8.5
Enrico Tassi
2015-03-09
Initial commit
Enrico Tassi