aboutsummaryrefslogtreecommitdiff
path: root/pretyping/recordops.mli
AgeCommit message (Expand)Author
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-04-26Misc small fixes : warning, dep cycles, ocamlbuild...letouzey
2009-11-04Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.gmelquio
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-01-17DISCLAIMERpuech
2008-11-05Move Record desugaring to constrintern and add ability to use notationsmsozeau
2008-08-05Suite 11187 et 11298 : ne retarder le dépliage d'une projectionherbelin
2008-06-29Préférence donnée aux constantes qui ne sont pas des projectionsherbelin
2008-02-19added products and sorts as possible heads for canonical structurescorbinea
2008-02-14Added default canonical structures (see example in test-suite)corbinea
2006-08-24Morceau de code mortherbelin
2006-07-07Correction bug 1172 + correction en passant de la taille des paramètres de f...herbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2005-02-12Ajout Print Canonical Structuresherbelin
2004-11-19Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIREherbelin
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-07-16Nouvelle en-têteherbelin
2004-06-25correspondance des records et noms de champs de records entre un module et sa...letouzey
2003-06-10Ajout notation c.(f) en v8 pour les projections de Recordherbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2001-11-05GROS COMMIT:barras
2001-10-16Nettoyage Recordobj et conséquencesherbelin
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-03-15entetesfilliatr
2001-02-05Restructuration de classops; évolution en une version mieux intégrée au re...herbelin
2000-12-19Export fonction testant si un inductive est un recordherbelin
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-11-02suppression des (* open Generic *)filliatr
2000-09-10Correction pour make docherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-01-11Ajout de Recordherbelin
1999-12-03 - global_reference traite des variablesfilliatr
1999-11-24Versions initialesherbelin