index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
typeclasses.ml
Commit message (
Expand
)
Author
Age
*
Restore backward compatibility. ":>" declares subinstances in Class declarati...
msozeau
2011-11-18
*
Fix for subclasses implementation, allowing to register generalized classes s...
msozeau
2011-11-18
*
Merge subinstances branch by me and Tom Prince.
msozeau
2011-11-17
*
Add type annotations around all calls to Libobject.declare_object
letouzey
2011-11-02
*
Fix bug #2557 and an issue with Propers for complement
msozeau
2011-10-07
*
- Make typeclass transparency information directly available
msozeau
2011-04-13
*
- Do not make constants with an assigned type polymorphic (wrong unfoldings).
msozeau
2011-04-13
*
- Add modulo_delta_types flag for unification to allow full
msozeau
2011-03-13
*
Keep information on which fields are subclasses in class declarations,
msozeau
2011-03-11
*
- Fix treatment of globality flag for typeclass instance hints (they
msozeau
2011-02-14
*
Misc improvements about evar_map
letouzey
2010-12-15
*
Fix bug #2321, allowing "_" named projections in classes. Not realizing
msozeau
2010-09-28
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Remove compile-command pragmas for emacs
letouzey
2010-05-19
*
Improved the efficiency of evars traverals thanks to a split of
herbelin
2010-05-13
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
Compute the correct generalization information when discharging a class
msozeau
2010-02-16
*
Fix [Existing Class] impl and add documentation. Fix computation of the
msozeau
2010-02-10
*
Added module sharing support for typeclasses and hints (pri_auto_tactic).
soubiran
2010-01-12
*
Fix handling of instance declarations in presence of let-ins (bug
msozeau
2010-01-01
*
Fix type class discharge again.
msozeau
2009-11-15
*
- Fix discharge bug in typeclasses: some constrs were not actually
msozeau
2009-11-06
*
Integrate a few improvements on typeclasses and Program from the equations br...
msozeau
2009-10-28
*
Fixes around typeclasses:
msozeau
2009-10-27
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Remove useless Liboject.export_function field
glondu
2009-09-17
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Death of "survive_module" and "survive_section" (the first one was
herbelin
2009-08-13
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
Use the proper unification flags in e_exact. This makes exact fail a bit
msozeau
2009-07-09
*
- Implementation of a new typeclasses eauto procedure based on success
msozeau
2009-04-27
*
Rewrite of Program Fixpoint to overcome the previous limitations:
msozeau
2009-03-28
*
On remplace evar_map par evar_defs (seul evar_defs est désormais exporté
aspiwack
2009-02-19
*
Correct a bug in commit 11659
puech
2009-01-16
*
Fix exponential behaviour of the typeclasses persistent objects. Drop
puech
2008-12-06
*
Fix bug #1943 and restrict the inference optimisation of Program to
msozeau
2008-09-15
*
Fix bug #1936: uncaught exception due to undefinable exceptions.
msozeau
2008-09-14
*
Fix bug #1940: uncaught exception when searching for a type class.
msozeau
2008-09-14
*
Fix implementation of "Global Instance" which redeclared the same
msozeau
2008-08-27
*
Fix bug in term dnet preventing some unifications. Allow "higher-order"
msozeau
2008-07-28
*
Even better test for choosing rewrite or setoid_rewrite.
msozeau
2008-07-26
*
Correct implementation of discharging of implicit arguments and add new
msozeau
2008-07-22
*
Fixes in handling of implicit arguments:
msozeau
2008-07-04
*
Various bug fixes in type classes and subtac:
msozeau
2008-07-01
*
Code cleanup in typeclasses, remove dead and duplicated code.
msozeau
2008-06-21
*
Fix bug in handling of classes and instances inside sections at
msozeau
2008-06-17
*
Optionally (and by default) split typeclasses evars into connected
msozeau
2008-06-11
*
Fixes incorrect handling of existing existentials variables in
msozeau
2008-06-03
[next]