aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/impargs.mli
Commit message (Expand)AuthorAge
* Fix printing of projections with implicits.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* New Arguments vernacularGravatar gareuselesinge2011-11-21
* More comments and less doublons in some mliGravatar pboutill2011-02-10
* Export definition of type implicits_list for contribs + fixed aGravatar herbelin2010-10-05
* Added multiple implicit arguments rules per name.Gravatar herbelin2010-10-03
* Dead code in impargs (afaics, no more need, since r11242, to mergeGravatar herbelin2010-10-03
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Add doc for [Print Opaque Dependencies] and a better explanation for theGravatar msozeau2009-06-26
* Stop using a "Manual Implicit Arguments" flag and support them as soonGravatar msozeau2009-05-27
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* In manual implicit arguments mode, do not enrich implicitsGravatar msozeau2008-09-14
* Correct implementation of discharging of implicit arguments and add newGravatar msozeau2008-07-22
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Add the ability to specify the implicit status of section variables andGravatar msozeau2008-04-02
* Do a second pass on the treatment of user-given implicit arguments. NowGravatar msozeau2008-03-15
* Implicit arguments in class field declarationsGravatar msozeau2008-01-02
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Nouveaux changements autour des implicites (notamment suite àGravatar herbelin2007-05-06
* Multiples changements autour des implicites :Gravatar herbelin2007-04-29
* Nouvelle approche pour le discharge modulaireGravatar herbelin2007-01-10
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* Nouvelle en-têteGravatar herbelin2004-07-16
* Utilisation de noms dans 'Implicit Arguments [...]'Gravatar herbelin2003-09-23
* Mise en place d'implicites par noms en v8Gravatar herbelin2003-09-21
* Affichage forcé des implicites contextuels si pas de contexte connuGravatar herbelin2003-04-10
* Synchronisation séparée des implicites pour l'affichage du traducteur;Gravatar herbelin2003-04-09
* Correction Show ImplicitsGravatar herbelin2003-04-09
* Réorganisation de Impargs + mise en place d'une infrastructureGravatar herbelin2003-04-09
* Ajout des options "Set Contextual Implicits" et "Set Strict ImplicitsGravatar herbelin2002-12-02
* Des critères plus fins d'analyse des implicites automatiques; meilleur affic...Gravatar herbelin2002-10-28
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09