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