index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
FSets
Commit message (
Expand
)
Author
Age
*
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
*
Unset Asymmetric Patterns
pboutill
2013-01-18
*
No more constant named "int" in Coq theories (cf bug #2878)
letouzey
2012-12-18
*
Ltac repeat is in fact already doing progress
letouzey
2012-10-01
*
Kills the useless tactic annotations "in |- *"
letouzey
2012-07-05
*
Open Local Scope ---> Local Open Scope, same with Notation and alii
letouzey
2012-07-05
*
ZArith + other : favor the use of modern names instead of compat notations
letouzey
2012-07-05
*
Intuition: temporary(?) restore the unconditional unfolding of not
letouzey
2012-05-15
*
Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).
herbelin
2012-04-15
*
Final part of moving Program code inside the main code. Adapted add_definitio...
msozeau
2012-03-14
*
Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...
msozeau
2012-01-31
*
Tentative to fix bug #2628 by not letting intuition break records. Might be t...
msozeau
2012-01-28
*
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
*
- 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
*
Fix compilation issues.
msozeau
2011-02-16
*
- Fix treatment of globality flag for typeclass instance hints (they
msozeau
2011-02-14
*
s/appartness/membership/g (Closes: #2470)
glondu
2011-01-06
*
Cosmetic : let's take advantage of the n-ary exists notation
letouzey
2010-12-17
*
FMapFacts: typo noticed by Aaron
letouzey
2010-10-22
*
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
*
Reverted 13293 commited mistakenly. Sorry for the noise.
herbelin
2010-07-18
*
Tentative de suppression de l'import automatique des hints et coercions.
herbelin
2010-07-18
*
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
*
fsetdec: a forgotten Set instead of Type was breaking discard_nonFset (fix #2...
letouzey
2010-06-18
*
fsetdec: clear dependent hypothesis before anything else (fix #2136).
letouzey
2010-06-17
*
Made option "Automatic Introduction" active by default before too many
herbelin
2010-06-08
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
CompSpecType, a clone of CompSpec but in Type instead of Prop
letouzey
2010-02-12
*
Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*
letouzey
2010-01-07
*
Include can accept both Module and Module Type
letouzey
2010-01-07
*
Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...
letouzey
2009-12-09
*
Better visibility of the inductive CompSpec used to specify comparison functions
letouzey
2009-11-03
*
OrderedType implementation for various numerical datatypes + min/max structures
letouzey
2009-11-03
*
List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F...
letouzey
2009-11-02
*
Remove various useless {struct} annotations
letouzey
2009-11-02
*
FSetCompat: a compatibility wrapper between FSets and MSets
letouzey
2009-10-20
*
Merge SetoidList2 into SetoidList.
letouzey
2009-10-19
*
Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet...
letouzey
2009-10-16
*
MSets: a new generation of FSets
letouzey
2009-10-13
*
Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'
letouzey
2009-10-08
[next]