index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
MSets
Commit message (
Expand
)
Author
Age
*
Make standard library independent of the names generated by
Hugo Herbelin
2014-06-04
*
Making those proofs which depend on names generated for the arguments
Hugo Herbelin
2014-06-01
*
Restore implicit arguments of irreflexivity (fixes bug #3305).
Matthieu Sozeau
2014-05-09
*
Try a new way of handling template universe levels
Matthieu Sozeau
2014-05-06
*
- Fix arity handling in retyping (de Bruijn bug!)
Matthieu Sozeau
2014-05-06
*
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
*
Correct rebase on STM code. Thanks to E. Tassi for help on dealing with
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Cbn is happier when ?SetPositive fixpoints have the set as recursive argument
Pierre Boutillier
2014-05-02
*
Eta contractions to please cbn
Pierre Boutillier
2014-05-02
*
"Boolean Equality" and "Case Analysis" are already off by default...
letouzey
2013-07-17
*
No more constant named "int" in Coq theories (cf bug #2878)
letouzey
2012-12-18
*
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: a tail-recursive plength
letouzey
2012-08-06
*
induction/destruct : nicer syntax for generating equations (solves #2741)
letouzey
2012-07-09
*
MSetRBT : elementary arith proofs instead of calls to lia
letouzey
2012-07-05
*
ZArith + other : favor the use of modern names instead of compat notations
letouzey
2012-07-05
*
MSetRBT : implementation of MSets via Red-Black trees
letouzey
2012-04-13
*
MSetAVL: better implementation of filter suggested by X. Leroy
letouzey
2012-01-17
*
theories/, plugins/ and test-suite/ ported to the Arguments vernacular
gareuselesinge
2011-11-21
*
MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_right
letouzey
2011-10-14
*
fsetdec : non-atomic elements are now transformed as variables first (fix #2464)
letouzey
2011-10-07
*
Improved handling of element equalities in fsetdec (fix #2467)
letouzey
2011-10-07
*
Modularization of BinInt, related fixes in the stdlib
letouzey
2011-05-05
*
CompareSpec: a slight generalization/reformulation of CompSpec
letouzey
2011-03-17
*
- Add modulo_delta_types flag for unification to allow full
msozeau
2011-03-13
*
- Use transparency information all the way through unification and
msozeau
2011-02-17
*
s/appartness/membership/g (Closes: #2470)
glondu
2011-01-06
*
Extraction: re-introduce some eta-expansions in rare situations leading to '_...
letouzey
2010-09-20
*
For the moment, two small manual eta-expansions to avoid '_a after extraction
letouzey
2010-09-17
*
Made notations for exists, exists! and notations of Utf8.v recursive notations
herbelin
2010-07-22
*
MSetPositive: mention MSetInterface instead of FSetInterface
letouzey
2010-07-16
*
FSetPositive: sets of positive inspired by FMapPositive.
letouzey
2010-07-16
*
FSets/Msets: some renaming of module params to simplify the task of the extra...
letouzey
2010-07-05
*
Report fixes from FSetDecide to MSetDecide
letouzey
2010-06-18
*
MSetInterface: no induction principle about a Record (nicer extraction)
letouzey
2010-06-16
*
MSetAVL: for nicer extraction, we create only tree_ind, not tree_rect and tre...
letouzey
2010-06-15
*
Made option "Automatic Introduction" active by default before too many
herbelin
2010-06-08
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Change definition of FSetList so that equality is Leibniz
glondu
2010-04-09
*
CompSpecType, a clone of CompSpec but in Type instead of Prop
letouzey
2010-02-12
*
MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu)
letouzey
2010-01-12
*
Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*
letouzey
2010-01-07
*
Include can accept both Module and Module Type
letouzey
2010-01-07
*
MSetInterface: more modularity
letouzey
2010-01-07
*
MSetAVL: hints made local since some of them are quite violent (transitivity)
letouzey
2010-01-07
*
Avoid declaring hints about refl/sym/trans of eq in DecidableType2
letouzey
2010-01-05
*
Specific syntax for Instances in Module Type: Declare Instance
letouzey
2010-01-04
*
Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...
letouzey
2009-12-09
[next]