aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/discharge.ml
Commit message (Expand)AuthorAge
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Reuse the typing_flags datatype for inductives.Gravatar Pierre-Marie Pédrot2016-06-18
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
* | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* | Renaming variants of Entries.local_entryGravatar Matej Kosik2016-02-16
* | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\ \
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
|/ /
* | Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
| * Add a corresponding field in `mutual_inductive_entry` (part 1).Gravatar Arnaud Spiwack2015-06-24
|/
* 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