| Commit message (Expand) | Author | Age |
... | |
* | - Documentation des nouvelles options d'implicites (Set Strongly Strict | herbelin | 2008-02-06 |
* | Implicit arguments in class field declarations | msozeau | 2008-01-02 |
* | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau | 2007-12-31 |
* | Factorisation des opérations sur le type option de Util dans un module | aspiwack | 2007-12-05 |
* | Par compatibilité, les implicites terminaux sont maximaux aussi quand | herbelin | 2007-05-22 |
* | Correction bug calcul des implicites en présence d'evars dans les types | herbelin | 2007-05-16 |
* | Nouveaux changements autour des implicites (notamment suite à | herbelin | 2007-05-06 |
* | Multiples changements autour des implicites : | herbelin | 2007-04-29 |
* | Suite commit restructuration discharge (application du type de | herbelin | 2007-01-10 |
* | Nouvelle approche pour le discharge modulaire | herbelin | 2007-01-10 |
* | Évitement noms de constructeurs dans les motifs de filtrage de "match" (suite) | herbelin | 2006-12-09 |
* | Extension du polymorphisme de sorte au cas des définitions dans Type. | herbelin | 2006-10-28 |
* | Nouvelle implantation du polymorphisme de sorte pour les familles inductives | herbelin | 2006-05-23 |
* | Ajout array_fold_map', list_fold_map' et list_remove_first | herbelin | 2006-03-29 |
* | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin | 2005-12-26 |
* | Nettoyage suite à la détection par défaut des variables inutilisées par o... | herbelin | 2005-11-08 |
* | Moving centralised discharge into dispatched discharge_function; required to ... | herbelin | 2005-02-18 |
* | HUGE COMMIT | sacerdot | 2005-01-03 |
* | IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name). | sacerdot | 2004-11-16 |
* | Nouvelle en-tête | herbelin | 2004-07-16 |
* | Deplacement de iter_constr_with_full_binders dans Termops | herbelin | 2003-10-22 |
* | Correction du bug 335 et Export/Require Export dans un module | coq | 2003-10-07 |
* | Utilisation de noms dans 'Implicit Arguments [...]' | herbelin | 2003-09-23 |
* | Mise en place d'implicites par noms en v8 | herbelin | 2003-09-21 |
* | Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c... | herbelin | 2003-09-12 |
* | Nouvelle mouture du traducteur v7->v8 | herbelin | 2003-08-11 |
* | code mort | herbelin | 2003-06-10 |
* | Affichage forcé des implicites contextuels si pas de contexte connu | herbelin | 2003-04-10 |
* | Synchronisation séparée des implicites pour l'affichage du traducteur; | herbelin | 2003-04-09 |
* | Correction Show Implicits | herbelin | 2003-04-09 |
* | Gestion synchronisation des Impargs.*_out et des Impargs._strict dans Impargs | herbelin | 2003-04-09 |
* | Synchronisation avec reset | herbelin | 2003-04-09 |
* | Réorganisation de Impargs + mise en place d'une infrastructure | herbelin | 2003-04-09 |
* | Ajout des options "Set Contextual Implicits" et "Set Strict Implicits | herbelin | 2002-12-02 |
* | Analyse plus fine des occurrences rigides | herbelin | 2002-11-18 |
* | Prise en compte let-in | herbelin | 2002-10-29 |
* | Des critères plus fins d'analyse des implicites automatiques; meilleur affic... | herbelin | 2002-10-28 |
* | Nettoyage | herbelin | 2002-10-12 |
* | Modules dans COQ\!\!\!\! | coq | 2002-08-02 |
* | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin | 2002-05-29 |
* | Déplacement et export de type_of_global dans Global | herbelin | 2001-11-09 |
* | corrections mineures suite au commit de restructuration du noyau | barras | 2001-11-06 |
* | GROS COMMIT: | barras | 2001-11-05 |
* | Reorganisation de Goption. Passage des options l'utilisant en synchrone | letouzey | 2001-10-30 |
* | Suppression des arguments sur les constantes, inductifs et constructeurs | barras | 2001-10-09 |
* | Protection contre des arguments farfelus pour les implicites manuels | herbelin | 2001-09-21 |
* | entetes | filliatr | 2001-03-15 |
* | Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref | herbelin | 2001-02-07 |
* | Ré-introduction des implicites à la volée dans la définition des inductifs | herbelin | 2001-01-27 |
* | certains effets disparaissent a la sortie des sections, d'autres non (selon S... | filliatr | 2000-11-24 |