| Commit message (Expand) | Author | Age |
|---|
| * | This big commit addresses two problems: |  soubiran | 2009-10-21 |
| * | Delete trailing whitespaces in all *.{v,ml*} files |  glondu | 2009-09-17 |
| * | Add doc for [Print Opaque Dependencies] and a better explanation for the |  msozeau | 2009-06-26 |
| * | Stop using a "Manual Implicit Arguments" flag and support them as soon | msozeau | 2009-05-27 |
| * | Rewrite of Program Fixpoint to overcome the previous limitations: | msozeau | 2009-03-28 |
| * | In manual implicit arguments mode, do not enrich implicits | msozeau | 2008-09-14 |
| * | Correct implementation of discharging of implicit arguments and add new | msozeau | 2008-07-22 |
| * | Fixes in handling of implicit arguments: | msozeau | 2008-07-04 |
| * | Add the ability to specify the implicit status of section variables and | msozeau | 2008-04-02 |
| * | Do a second pass on the treatment of user-given implicit arguments. Now | msozeau | 2008-03-15 |
| * | 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 |
| * | Nouveaux changements autour des implicites (notamment suite à |  herbelin | 2007-05-06 |
| * | Multiples changements autour des implicites : | herbelin | 2007-04-29 |
| * | Nouvelle approche pour le discharge modulaire | herbelin | 2007-01-10 |
| * | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin | 2005-12-26 |
| * | Moving centralised discharge into dispatched discharge_function; required to ... | herbelin | 2005-02-18 |
| * | Nouvelle en-tête | herbelin | 2004-07-16 |
| * | Utilisation de noms dans 'Implicit Arguments [...]' | herbelin | 2003-09-23 |
| * | Mise en place d'implicites par noms en v8 | herbelin | 2003-09-21 |
| * | 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 |
| * | 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 |
| * | Des critères plus fins d'analyse des implicites automatiques; meilleur affic... | herbelin | 2002-10-28 |
| * | 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 |
| * | Suites modifs du noyau. Univ devient purement fonctionnel. |  barras | 2001-11-12 |
| * | GROS COMMIT: | barras | 2001-11-05 |
| * | Suppression des arguments sur les constantes, inductifs et constructeurs | barras | 2001-10-09 |
| * | entetes |  filliatr | 2001-03-15 |
| * | Ré-introduction des implicites à la volée dans la définition des inductifs | herbelin | 2001-01-27 |
| * | syntaxe AST Inversion + commentaires ocamlweb autour de $ | filliatr | 2000-12-12 |
| * | implicites manuels | filliatr | 2000-11-21 |
| * | separation calcul des implicites et declaration des constantes / inductifs / ... | filliatr | 2000-11-21 |
| * | Ajout implicits_of_global + accès par noms longs | herbelin | 2000-11-20 |
| * | L'état implicite des définitions survivant au discharge redevient celui du ... | herbelin | 2000-10-23 |
| * | suppression de Fw pour les implicites | herbelin | 2000-05-03 |
| * | modifs pour premiere edition de liens | filliatr | 1999-12-02 |
| * | Intégration du Termast et du Retyping de HH, et modifications connexes | herbelin | 1999-12-01 |
| * | poursuite de Vernacentries | filliatr | 1999-12-01 |
| * | module Termast | filliatr | 1999-11-26 |
| * | - un effort sur la doc (ocamlweb) | filliatr | 1999-09-19 |
soubiran
glondu
msozeau
herbelin
coq
barras
filliatr