index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
MSets
/
MSetGenTree.v
Commit message (
Expand
)
Author
Age
*
Ensuring all .v files end with a newline to make "sed -i" work better on them.
Hugo Herbelin
2017-08-21
*
Prelude : no more autoload of plugins extraction and recdef
Pierre Letouzey
2017-06-14
*
Revert "Temporary hack to compensate missing comma while re-printing tactic"
Hugo Herbelin
2016-04-27
*
Temporary hack to compensate missing comma while re-printing tactic
Hugo Herbelin
2016-04-27
*
Simpl less (so that cbn will not simpl too much)
Pierre Boutillier
2014-10-01
*
Keyed unification option, compiling the whole standard library
Matthieu Sozeau
2014-09-27
*
Arith: full integration of the "Numbers" modular framework
Pierre Letouzey
2014-07-09
*
Avoid using a deprecated lemma in the standard library.
Guillaume Melquiond
2014-06-26
*
- Fix arity handling in retyping (de Bruijn bug!)
Matthieu Sozeau
2014-05-06
*
Correct rebase on STM code. Thanks to E. Tassi for help on dealing with
Matthieu Sozeau
2014-05-06
*
"Boolean Equality" and "Case Analysis" are already off by default...
letouzey
2013-07-17
*
Change Hint Resolve, Immediate to take a global reference as argument
msozeau
2012-10-26
*
Ltac repeat is in fact already doing progress
letouzey
2012-10-01
*
MSetRBT : implementation of MSets via Red-Black trees
letouzey
2012-04-13