aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/discharge.ml
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
* Fix infer conv using the wrong universe conversion flexibility informationGravatar Matthieu Sozeau2014-08-03
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* - Do module substitution inside mind_record.Gravatar Matthieu Sozeau2014-07-25
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Removing useless casts between arrays and lists.Gravatar ppedrot2013-08-04
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Minor code cleaning in CArray / CList.Gravatar ppedrot2013-03-23
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Noise for nothingGravatar pboutill2012-03-02
* Fixing critical part of bug #2504. Not all inductive types in Type areGravatar herbelin2011-10-01
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Petites corrections vis à vis des commits 10860, 10859, 10850Gravatar herbelin2008-04-28
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* Types inductifs parametriquesGravatar mohring2005-11-02
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* 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
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* 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
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* Tables logarithmiques pour les coercions + nettoyageGravatar herbelin2003-06-08
* Réorganisation de Impargs + mise en place d'une infrastructureGravatar herbelin2003-04-09
* la table PARAMETER n'existe plus (mergé dans la table CONSTANT)Gravatar letouzey2002-12-03
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Renoncement à distinguer les types "constr" et "types"; nettoyageGravatar herbelin2002-08-13
* 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
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14
* compat ocaml 3.03Gravatar filliatr2001-12-13
* Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantGravatar herbelin2001-11-20
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* corrections mineures suite au commit de restructuration du noyauGravatar barras2001-11-06
* GROS COMMIT:Gravatar barras2001-11-05
* Abstraction de l'immplementation de dirpath et implementation dans l'autre se...Gravatar herbelin2001-10-17
* Suppression option immediate_discharge; nettoyage de Declare et conséquencesGravatar herbelin2001-10-11
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09