aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
* Fixing a bug in 11804 (support for _ in ident entry of notations). Gravatar herbelin2009-01-20
* - Structuring Numbers and fixing Setoid in stdlib's doc.Gravatar herbelin2009-01-19
* DISCLAIMERGravatar puech2009-01-17
* Switched to "standardized" names for the properties of eq andGravatar herbelin2009-01-01
* - 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
* 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
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
* Dumpglob.dump_modref : fix an assert failureGravatar letouzey2008-10-14
* Backporting 11445 from 8.2 to trunk (negative conditions inGravatar herbelin2008-10-11
* Améliorations de l'affichage des coercions suggérées par Georges :Gravatar herbelin2008-10-08
* Fix bug #1943 and restrict the inference optimisation of Program toGravatar msozeau2008-09-15
* 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
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Suite commit 11236Gravatar notin2008-07-24
* Stop glob messages to be printed by default on stdout Gravatar letouzey2008-07-23
* Correct implementation of discharging of implicit arguments and add newGravatar msozeau2008-07-22
* Oubli lors du commit #11236Gravatar notin2008-07-22
* Suite commit 11236Gravatar notin2008-07-21
* Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...Gravatar notin2008-07-18
* Modification rapide du message d'erreur lorsqu'un _ ne peut êtreGravatar herbelin2008-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
* - Improve [Context] vernacular to allow arbitrary binders, not justGravatar msozeau2008-07-07
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Documentation Prop<=Set et Arguments Scope GlobalGravatar herbelin2008-07-01
* 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
* Correction bug 1878 (utilisation de extend_evar déplacée là où uneGravatar herbelin2008-06-14
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* 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
* Notation concise pour la valeur par défaut des cas reconnus commeGravatar herbelin2008-05-28
* Ajout de la possibilité d'utiliser fix/cofix dans les notations.Gravatar herbelin2008-05-24
* Fix "not an applied typeclass" error for legitimate classesGravatar msozeau2008-05-12
* - Prise en compte de l'unicode dans la fonction hdchar (elle fournissait desGravatar herbelin2008-05-10
* Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757Gravatar herbelin2008-05-07
* Better parsing of typeclasses, any constr is allowed for ! bindings soGravatar msozeau2008-05-06
* 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