| Commit message (Expand) | Author | Age |
* | Plus de combinateurs sont passés de Util à Option. Le module Options | aspiwack | 2007-12-06 |
* | Prise en compte des notations "alias" dans la globalisation des coercions. | herbelin | 2007-11-08 |
* | Added the automatic generation of the boolean equality if possible and the | vsiles | 2007-10-05 |
* | Modification of the Scheme command. | vsiles | 2007-09-28 |
* | Uniformisation politique de nommage evd/isevars (evd si evar_defs, | herbelin | 2007-09-06 |
* | Utilisation plus précise de la contrainte de type pour interpréter les | herbelin | 2007-08-24 |
* | If a fixpoint is not written with an explicit { struct ... }, then | letouzey | 2007-07-07 |
* | Modification of VernacScheme to handle a new scheme: Equality (equality in | vsiles | 2007-05-25 |
* | Nettoyage et standardisation des messages d'erreurs. | herbelin | 2007-05-17 |
* | New keyword "Inline" for Parameters and Axioms for automatic | soubiran | 2007-04-25 |
* | 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-04-17 |
* | Add a parameter to QuestionMark evar kind to say it can be turned into an obl... | msozeau | 2007-03-19 |
* | Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo... | herbelin | 2007-02-24 |
* | Vérification que toutes les evars ont étés instanciées dans les types imp... | herbelin | 2007-02-07 |
* | Addition of a "Combined Scheme" vernacular command for building the conjuncti... | msozeau | 2006-12-23 |
* | Correction du bug #1273, deuxième version (avec des shémas d'elimination pl... | notin | 2006-12-12 |
* | Extension du polymorphisme de sorte au cas des définitions dans Type. | herbelin | 2006-10-28 |
* | Report de l'heuristique d'unification premier ordre flexible/rigide | herbelin | 2006-09-15 |
* | Retour à un warning en cas de (co-)fixpoint pas totalement mutuel | herbelin | 2006-09-09 |
* | Finalement, interdiction des points fixes non totalement mutuellement | herbelin | 2006-09-06 |
* | 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-09-01 |
* | The "clean integration of subtac" patch. | msozeau | 2006-05-29 |
* | Nouvelle implantation du polymorphisme de sorte pour les familles inductives | herbelin | 2006-05-23 |
* | Si un fixpoint a plusieurs arguments, mais un seul de type inductif, | letouzey | 2006-04-14 |
* | Finalement, scopes utiles pour option 'where' (cf bug #1132) | herbelin | 2006-04-07 |
* | Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}. | msozeau | 2006-03-13 |
* | Correction du bug 808: il est maintenant interdit de déclarer une assomption... | coq | 2006-03-02 |
* | Bug correction in saving proofs: If a hook opens a proof but does not close i... | bertot | 2006-02-13 |
* | warning seulement si mode verbose | herbelin | 2006-02-06 |
* | 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 |
* | Orthographe de 'instantiate' | herbelin | 2005-12-17 |
* | Changement des named_context | gregoire | 2005-12-02 |
* | Nettoyage suite à la détection par défaut des variables inutilisées par o... | herbelin | 2005-11-08 |
* | Types inductifs parametriques | mohring | 2005-11-02 |
* | Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p... | herbelin | 2005-01-02 |
* | Rétablissement d'un vrai Eval sous le contexte des définitions, pas un qui ... | herbelin | 2004-12-30 |
* | Bug (cf #892) | herbelin | 2004-12-06 |
* | IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name). | sacerdot | 2004-11-16 |
* | Changement dans les boxed values . | gregoire | 2004-11-12 |
* | COMMITED BYTECODE COMPILER | barras | 2004-10-20 |
* | Suppression IsConjecture redondant avec Conjectural | herbelin | 2004-10-11 |
* | hiding the meta_map in evar_defs | barras | 2004-09-15 |
* | 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 |