aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/record.mli
Commit message (Expand)AuthorAge
* Update headers.Gravatar Maxime Dénès2015-01-12
* Pass around information on the use of template polymorphism forGravatar Matthieu Sozeau2014-11-23
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Rework typeclass resolution and control of backtracking.Gravatar Matthieu Sozeau2014-09-15
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* 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
* Restore backward compatibility. ":>" declares subinstances in Class declarati...Gravatar msozeau2011-11-18
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
* 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
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Les records déclarés avec Record ne peuvent plus être récursifs (le Gravatar aspiwack2009-01-19
* DISCLAIMERGravatar puech2009-01-17
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* Fixed bug #2006 (type constraint on Record was not taken into account) +Gravatar herbelin2008-11-23
* Fix mixup between Record, Structure and Class by adding a new variant forGravatar msozeau2008-11-10
* More factorization of inductive/record and typeclasses: move classGravatar msozeau2008-11-09
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Nouvelle syntaxe pour écrire des records (co)inductifs :Gravatar aspiwack2008-11-05
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* Fix bugs that were reopened due to the change of setoidGravatar msozeau2008-03-08
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* Nouvelle en-têteGravatar herbelin2004-07-16
* meilleure presentation des commentaires du traducteurGravatar barras2004-01-02
* Mise en place possibilité de définitions locales dans les paramètres des r...Gravatar herbelin2003-09-06
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intgration uniforme de coercions dans les dclarations (Variable and co) et re...Gravatar herbelin2002-06-03
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Utilisation des de Bruijn pour la constructions des records et de leur projec...Gravatar herbelin2002-05-13
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* entetesGravatar filliatr2001-03-15
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...Gravatar herbelin2001-01-24
* Ajout de constantes locales dans les RecordsGravatar herbelin2001-01-24
* Découpage des différentes fonctionnalités de build_mutual et definition_st...Gravatar herbelin2000-12-19
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Ajout de RecordGravatar herbelin2000-01-11
* - global_reference traite des variablesGravatar filliatr1999-12-03
* Version initialeGravatar herbelin1999-12-02