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
*
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
*
integrate MSetToFiniteSet into the compilation (and fix it)
letouzey
2009-12-08
*
Fix backtracking heuristic in typeclass resolution.
msozeau
2009-11-30
*
Fix [Instance: forall ..., C args := t] declarations to behave as
msozeau
2009-11-15
*
Use generalizable variables info when internalizing arbitrary bindings,
msozeau
2009-11-08
*
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
*
Add a new vernacular command for controling implicit generalization of
msozeau
2009-10-27
*
MSetInterface: some explicit types to avoid Raw.t-instead-of-t effect
letouzey
2009-10-21
*
OrderedType2 : trivial lemmas are turned into tests for order.
letouzey
2009-10-16
*
Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet...
letouzey
2009-10-16
*
MSetInterface: (W)Raw2Sets splitted in 2 (helps a future commit by Elie)
letouzey
2009-10-15
*
OrderedType2.order is slightly weaker since last commit, adapt accordingly
letouzey
2009-10-15
*
MSets: a new generation of FSets
letouzey
2009-10-13