aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/recordops.mli
Commit message (Expand)AuthorAge
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Documenting check_record + changing a possibly undefined int into int option.Gravatar Hugo Herbelin2014-12-15
* - Fixes for canonical structure resolution (check that the initial term indee...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
* Stack operations of Reductionops in Reductionops.StackGravatar Pierre Boutillier2014-02-24
* Unplugging Autoinstance. The code is still here if someone wishesGravatar ppedrot2013-09-12
* Misc changes around coqtop.ml :Gravatar letouzey2013-08-22
* Modulification of nameGravatar ppedrot2012-12-18
* Unification in Evar_conv uses an abstract machine stateGravatar pboutill2012-08-09
* Updating headers.Gravatar herbelin2012-08-08
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Improved check is_open_canonical_projectionGravatar gareuselesinge2011-11-08
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Applying François' patches about Canonical Projections (see #2302 and #2334).Gravatar herbelin2010-06-26
* 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
* Misc small fixes : warning, dep cycles, ocamlbuild...Gravatar letouzey2010-04-26
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* DISCLAIMERGravatar puech2009-01-17
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Suite 11187 et 11298 : ne retarder le dépliage d'une projectionGravatar herbelin2008-08-05
* Préférence donnée aux constantes qui ne sont pas des projectionsGravatar herbelin2008-06-29
* added products and sorts as possible heads for canonical structuresGravatar corbinea2008-02-19
* Added default canonical structures (see example in test-suite)Gravatar corbinea2008-02-14
* Morceau de code mortGravatar herbelin2006-08-24
* Correction bug 1172 + correction en passant de la taille des paramètres de f...Gravatar herbelin2006-07-07
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* Ajout Print Canonical StructuresGravatar herbelin2005-02-12
* Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIREGravatar herbelin2004-11-19
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* Nouvelle en-têteGravatar herbelin2004-07-16
* correspondance des records et noms de champs de records entre un module et sa...Gravatar letouzey2004-06-25
* Ajout notation c.(f) en v8 pour les projections de RecordGravatar herbelin2003-06-10
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* GROS COMMIT:Gravatar barras2001-11-05
* Nettoyage Recordobj et conséquencesGravatar herbelin2001-10-16
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* entetesGravatar filliatr2001-03-15
* Restructuration de classops; évolution en une version mieux intégrée au re...Gravatar herbelin2001-02-05
* Export fonction testant si un inductive est un recordGravatar herbelin2000-12-19
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Correction pour make docGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10