| Age | Commit message (Expand) | Author |
|---|
| 2007-05-17 | Nettoyage et standardisation des messages d'erreurs. | herbelin |
| 2007-04-25 | New keyword "Inline" for Parameters and Axioms for automatic | soubiran |
| 2007-04-17 | Reorder hook and printing of message, more natural this way. | msozeau |
| 2007-04-17 | Added the option to set/unset the automatic generation of elimination schemes | vsiles |
| 2007-03-19 | Add a parameter to QuestionMark evar kind to say it can be turned into an obl... | msozeau |
| 2007-02-24 | Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo... | herbelin |
| 2007-02-07 | Vérification que toutes les evars ont étés instanciées dans les types imp... | herbelin |
| 2006-12-23 | Addition of a "Combined Scheme" vernacular command for building the conjuncti... | msozeau |
| 2006-12-12 | Correction du bug #1273, deuxième version (avec des shémas d'elimination pl... | notin |
| 2006-10-28 | Extension du polymorphisme de sorte au cas des définitions dans Type. | herbelin |
| 2006-09-15 | Report de l'heuristique d'unification premier ordre flexible/rigide | herbelin |
| 2006-09-09 | Retour à un warning en cas de (co-)fixpoint pas totalement mutuel | herbelin |
| 2006-09-06 | Finalement, interdiction des points fixes non totalement mutuellement | herbelin |
| 2006-09-01 | Ajout possibilité clause "where" dans co-points fixes | herbelin |
| 2006-09-01 | Extension et réorganisation de l'interprétation des (co-)points fixes | herbelin |
| 2006-05-29 | The "clean integration of subtac" patch. | msozeau |
| 2006-05-23 | Nouvelle implantation du polymorphisme de sorte pour les familles inductives | herbelin |
| 2006-04-14 | Si un fixpoint a plusieurs arguments, mais un seul de type inductif, | letouzey |
| 2006-04-07 | Finalement, scopes utiles pour option 'where' (cf bug #1132) | herbelin |
| 2006-03-13 | Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}. | msozeau |
| 2006-03-02 | Correction du bug 808: il est maintenant interdit de déclarer une assomption... | coq |
| 2006-02-13 | Bug correction in saving proofs: If a hook opens a proof but does not close i... | bertot |
| 2006-02-06 | warning seulement si mode verbose | herbelin |
| 2006-01-28 | Réorganisation de la structure interne des types de déclarations (decl_kinds) | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin |
| 2005-12-21 | Restructuration des points d'entrée de Pretyping et Constrintern | herbelin |
| 2005-12-17 | Orthographe de 'instantiate' | herbelin |
| 2005-12-02 | Changement des named_context | gregoire |
| 2005-11-08 | Nettoyage suite à la détection par défaut des variables inutilisées par o... | herbelin |
| 2005-11-02 | Types inductifs parametriques | mohring |
| 2005-01-02 | Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p... | herbelin |
| 2004-12-30 | Rétablissement d'un vrai Eval sous le contexte des définitions, pas un qui ... | herbelin |
| 2004-12-06 | Bug (cf #892) | herbelin |
| 2004-11-16 | IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name). | sacerdot |
| 2004-11-12 | Changement dans les boxed values . | gregoire |
| 2004-10-20 | COMMITED BYTECODE COMPILER | barras |
| 2004-10-11 | Suppression IsConjecture redondant avec Conjectural | herbelin |
| 2004-09-15 | hiding the meta_map in evar_defs | barras |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-06-25 | correspondance des records et noms de champs de records entre un module et sa... | letouzey |
| 2004-03-31 | Export de l'information si un inductive est un record ou non (pour xml) | herbelin |
| 2004-03-30 | Distinction entre declarations internes (p.ex. _subproof) et declarations uti... | herbelin |
| 2004-03-27 | Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo... | herbelin |
| 2004-03-05 | modif des fixpoints pour que si on donne une notation au produit, les pts fix... | barras |
| 2004-02-26 | Keep structure information for Fixpoint declaration and Fix terms | bertot |
| 2004-01-29 | Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :... | herbelin |
| 2004-01-13 | Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a... | herbelin |
| 2004-01-02 | meilleure presentation des commentaires du traducteur | barras |
| 2003-10-23 | Conjecture declare maintenant un axiome; reorganisation VernacDefinition | herbelin |
| 2003-10-14 | Changement 'as notation' en 'where notation'; Plus d'uniformite dans la gesti... | herbelin |
