aboutsummaryrefslogtreecommitdiff
path: root/toplevel/record.mli
AgeCommit message (Expand)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-01-19Les records déclarés avec Record ne peuvent plus être récursifs (le aspiwack
2009-01-17DISCLAIMERpuech
2008-12-31Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->herbelin
2008-11-23Fixed bug #2006 (type constraint on Record was not taken into account) +herbelin
2008-11-10Fix mixup between Record, Structure and Class by adding a new variant formsozeau
2008-11-09More factorization of inductive/record and typeclasses: move classmsozeau
2008-11-05Move Record desugaring to constrintern and add ability to use notationsmsozeau
2008-11-05Nouvelle syntaxe pour écrire des records (co)inductifs :aspiwack
2008-07-04Fixes in handling of implicit arguments:msozeau
2008-05-30Improvements on coqdoc by adding more information into .globmsozeau
2008-03-08Fix bugs that were reopened due to the change of setoidmsozeau
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2004-07-16Nouvelle en-têteherbelin
2004-01-02meilleure presentation des commentaires du traducteurbarras
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des r...herbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-06-03Intgration uniforme de coercions dans les dclarations (Variable and co) et re...herbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-13Utilisation des de Bruijn pour la constructions des records et de leur projec...herbelin
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-03-15entetesfilliatr
2001-02-14Mise en place d'un système optionnel de discharge immédiat; prise en compte...herbelin
2001-01-24Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...herbelin
2001-01-24Ajout de constantes locales dans les Recordsherbelin
2000-12-19Découpage des différentes fonctionnalités de build_mutual et definition_st...herbelin
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-01-11Ajout de Recordherbelin
1999-12-03 - global_reference traite des variablesfilliatr
1999-12-02Version initialeherbelin