aboutsummaryrefslogtreecommitdiff
path: root/library/impargs.ml
AgeCommit message (Expand)Author
2009-12-01Continuing r12485-12486 (cleaning around name generation)herbelin
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-10-26Local/Global revision 12418 continuedherbelin
2009-10-26New cleaning phase of the Local/Global option managementherbelin
2009-10-25Improved the treatment of Local/Global options (noneffective Local onherbelin
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Remove useless Liboject.export_function fieldglondu
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-13Death of "survive_module" and "survive_section" (the first one washerbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-06-01Prevent automatic inference of implicit arguments when the auto flag ismsozeau
2009-05-27Fix implicit args code so that declarations are added for allmsozeau
2009-05-27Stop using a "Manual Implicit Arguments" flag and support them as soonmsozeau
2009-03-28Rewrite of Program Fixpoint to overcome the previous limitations: msozeau
2009-01-23Petit nettoyage faisant suite au commit #11847 .aspiwack
2008-09-14In manual implicit arguments mode, do not enrich implicitsmsozeau
2008-07-24broke cyclic dependenciesbarras
2008-07-22Correct implementation of discharging of implicit arguments and add newmsozeau
2008-07-07Fix implicit arguments in sections bug and check for resolution of evars whenmsozeau
2008-07-04Fixes in handling of implicit arguments:msozeau
2008-04-15- Un peu de doc, préparation du CHANGES pour la release.herbelin
2008-04-02Add the ability to specify the implicit status of section variables andmsozeau
2008-03-15Do a second pass on the treatment of user-given implicit arguments. Nowmsozeau
2008-02-06- Documentation des nouvelles options d'implicites (Set Strongly Strictherbelin
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