aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/implicit_quantifiers.ml
Commit message (Expand)AuthorAge
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Fix bug #2262: bad implicit argument number by avoiding countingGravatar msozeau2010-06-09
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Fix implicit_application for let-bound variables in the class context.Gravatar msozeau2010-01-28
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Use generalizable variables info when internalizing arbitrary bindings,Gravatar msozeau2009-11-08
* Misc fixes.Gravatar msozeau2009-11-06
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
* Fix bug #2162 and a name clashing bug in generalized binders.Gravatar msozeau2009-10-09
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
* Generalized implementation of generalization.Gravatar msozeau2008-10-23
* Fix bugs #1975 and #1976.Gravatar msozeau2008-10-22
* A much better implementation of implicit generalization:Gravatar msozeau2008-10-22
* Affichage des notations récursives:Gravatar herbelin2008-10-22
* Fix bug #1943 and restrict the inference optimisation of Program toGravatar msozeau2008-09-15
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Code cleanup in typeclasses, remove dead and duplicated code.Gravatar msozeau2008-06-21
* Fix "not an applied typeclass" error for legitimate classesGravatar msozeau2008-05-12
* Better parsing of typeclasses, any constr is allowed for ! bindings soGravatar msozeau2008-05-06
* Add the ability to specify what to do with free variables in instanceGravatar msozeau2008-04-12
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* Enhance handling of parameters in typeclass constraints: permit to specify an...Gravatar msozeau2008-04-01
* - Fix for rewriting under dependent products.Gravatar msozeau2008-03-31
* Ajout d'abbréviations/notations paramétriquesGravatar herbelin2008-03-30
* Fix a bug found by B. Grégoire when declaring morphisms in moduleGravatar msozeau2008-03-23
* Do another pass on the typeclasses code. Correct globalization of classGravatar msozeau2008-03-19
* Move generally useful definition of nf_evar on contexts to evarutil.Gravatar msozeau2008-02-08
* Generalize instance declarations to any context, better name handling. Add ho...Gravatar msozeau2008-01-15
* Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp...Gravatar msozeau2008-01-07
* Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ...Gravatar msozeau2008-01-05
* Add partial setoids in theories/Classes, add SetoidDec class for setoids with...Gravatar msozeau2008-01-04
* Better resolution of implicit parameters in typeclass binders, add extensiona...Gravatar msozeau2008-01-02
* Fix name capture bug and call the right pretyper in subtac.Gravatar msozeau2007-12-31
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31