aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
Commit message (Expand)AuthorAge
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* 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
* - Structuring Numbers and fixing Setoid in stdlib's doc.Gravatar herbelin2009-01-19
* DISCLAIMERGravatar puech2009-01-17
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
* More factorization of inductive/record and typeclasses: move classGravatar msozeau2008-11-09
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Correct enormous bug in interpretation of generalized binders: it simplyGravatar msozeau2008-10-26
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
* Generalized implementation of generalization.Gravatar msozeau2008-10-23
* A much better implementation of implicit generalization:Gravatar msozeau2008-10-22
* Affichage des notations récursives:Gravatar herbelin2008-10-22
* Add enough information to correctly globalize recursive calls in inductive andGravatar msozeau2008-09-11
* Better handling of the opacity of proof obligations, add the possibility ofGravatar msozeau2008-09-07
* Suite commit 11236Gravatar notin2008-07-24
* Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...Gravatar notin2008-07-18
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Autour du parsing:Gravatar herbelin2008-07-15
* Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...Gravatar notin2008-07-07
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...Gravatar notin2008-06-25
* Code cleanup in typeclasses, remove dead and duplicated code.Gravatar msozeau2008-06-21
* Enhancements to coqdoc, better globalization of sections and modules.Gravatar msozeau2008-06-06
* Fix setoid_rewrite documentation examples.Gravatar msozeau2008-06-03
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* Postpone the search for the recursive argument index from the user givenGravatar msozeau2008-05-06
* Factorize code for internalization of binders to fix bug #1846. AlsoGravatar msozeau2008-05-04
* Correction bug List.map2 dans Case12.vGravatar herbelin2008-04-09
* Modifications diverses et variées :Gravatar herbelin2008-03-30
* Ajout d'abbréviations/notations paramétriquesGravatar herbelin2008-03-30
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
* Various fixes on typeclasses:Gravatar msozeau2008-03-27
* Finish fix in command where we still lost information on what was a typeGravatar msozeau2008-03-24
* Do a second pass on the treatment of user-given implicit arguments. NowGravatar msozeau2008-03-15
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...Gravatar msozeau2008-01-17
* Generalize instance declarations to any context, better name handling. Add ho...Gravatar msozeau2008-01-15
* Correction bug #1749 (datant de l'implantation des or-patterns) +Gravatar herbelin2008-01-05
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Uniformisation politique de nommage evd/isevars (evd si evar_defs,Gravatar herbelin2007-09-06
* - Débogueur: positionnement de set_detype_anonymous pour ne pasGravatar herbelin2007-08-29
* Slight cleanup of refl_omega.ml : in particular it uses now listGravatar letouzey2007-07-11
* Fix bug in subst_cases_pattern when aliasing recursive notations.Gravatar msozeau2007-07-02
* Nouveaux changements autour des implicites (notamment suite àGravatar herbelin2007-05-06
* Multiples changements autour des implicites :Gravatar herbelin2007-04-29
* Correction bug #1477 sur ordre des variables partagées par les or-patterns.Gravatar herbelin2007-04-13
* Support for implicit formal argument types in Program ; parse types in type s...Gravatar msozeau2007-03-28