| Commit message (Expand) | Author | Age |
|---|
| * | Generalized binding syntax overhaul: only two new binders: `() and `{}, |  msozeau | 2008-12-14 |
| * | Fixed bug #2006 (type constraint on Record was not taken into account) + |  herbelin | 2008-11-23 |
| * | Fix mixup between Record, Structure and Class by adding a new variant for | msozeau | 2008-11-10 |
| * | More factorization of inductive/record and typeclasses: move class | msozeau | 2008-11-09 |
| * | Move Record desugaring to constrintern and add ability to use notations | msozeau | 2008-11-05 |
| * | Nouvelle syntaxe pour écrire des records (co)inductifs : |  aspiwack | 2008-11-05 |
| * | Fix bug #1959 (remember: never use a partial functions mindlessly). | msozeau | 2008-10-08 |
| * | In manual implicit arguments mode, do not enrich implicits | msozeau | 2008-09-14 |
| * | Add enough information to correctly globalize recursive calls in inductive and | msozeau | 2008-09-11 |
| * | Uniformisation du format des messages d'erreur (commencent par une | herbelin | 2008-07-17 |
| * | Fix implicit arguments in sections bug and check for resolution of evars when | msozeau | 2008-07-07 |
| * | Fixes in handling of implicit arguments: | msozeau | 2008-07-04 |
| * | Improvements on coqdoc by adding more information into .glob | msozeau | 2008-05-30 |
| * | Postpone the search for the recursive argument index from the user given | msozeau | 2008-05-06 |
| * | Do a second pass on the treatment of user-given implicit arguments. Now | msozeau | 2008-03-15 |
| * | Fix bugs that were reopened due to the change of setoid | msozeau | 2008-03-08 |
| * | Syntax changes in typeclasses, remove "?" for usual implicit arguments | msozeau | 2008-03-06 |
| * | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau | 2007-12-31 |
| * | Plus de combinateurs sont passés de Util à Option. Le module Options | aspiwack | 2007-12-06 |
| * | - Ajout de la possibilité d'utiliser la notation Record pour les | herbelin | 2007-06-30 |
| * | Correction bug #1507 (report révision 9807 de v8.1 vers trunk) | herbelin | 2007-04-29 |
| * | Add a parameter to QuestionMark evar kind to say it can be turned into an obl... | msozeau | 2007-03-19 |
| * | Suppression argument pattern_source du case_info (code jamais utilisé) | herbelin | 2007-03-15 |
| * | Morceau de code mort | herbelin | 2006-08-24 |
| * | The "clean integration of subtac" patch. | msozeau | 2006-05-29 |
| * | Réorganisation de la structure interne des types de déclarations (decl_kinds) | herbelin | 2006-01-28 |
| * | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin | 2005-12-26 |
| * | Restructuration des points d'entrée de Pretyping et Constrintern | herbelin | 2005-12-21 |
| * | Changement des named_context |  gregoire | 2005-12-02 |
| * | Types inductifs parametriques |  mohring | 2005-11-02 |
| * | Moving centralised discharge into dispatched discharge_function; required to ... | herbelin | 2005-02-18 |
| * | compatibility with POWERPC | gregoire | 2004-11-22 |
| * | IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name). |  sacerdot | 2004-11-16 |
| * | COMMITED BYTECODE COMPILER |  barras | 2004-10-20 |
| * | Nouvelle en-tête | herbelin | 2004-07-16 |
| * | correspondance des records et noms de champs de records entre un module et sa... |  letouzey | 2004-06-25 |
| * | Export de l'information si un inductive est un record ou non (pour xml) | herbelin | 2004-03-31 |
| * | Distinction entre declarations internes (p.ex. _subproof) et declarations uti... | herbelin | 2004-03-30 |
| * | bugs avec Pose et Assert | barras | 2004-01-09 |
| * | meilleure presentation des commentaires du traducteur | barras | 2004-01-02 |
| * | (Re-)branchement sur les noms reserves pour les args d'inductif (dont Record) | herbelin | 2003-09-16 |
| * | Mise en place possibilité de définitions locales dans les paramètres des r... | herbelin | 2003-09-06 |
| * | Réforme de l'interprétation des termes : | herbelin | 2002-11-14 |
| * | Intégration des modifs de la branche mowgli : | herbelin | 2002-11-05 |
| * | retour en arriere concernant la recherche d'occurence modulo expansion des le... | barras | 2002-10-09 |
| * | Que des niveaux d'univers frais dans le type des constantes globales | herbelin | 2002-09-29 |
| * | Modules dans COQ\!\!\!\! |  coq | 2002-08-02 |
| * | Intgration uniforme de coercions dans les dclarations (Variable and co) et re... | herbelin | 2002-06-03 |
| * | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin | 2002-05-29 |
| * | Utilisation des de Bruijn pour la constructions des records et de leur projec... | herbelin | 2002-05-13 |
msozeau
herbelin
aspiwack
gregoire
mohring
sacerdot
barras
letouzey
coq