aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/declarations.ml
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* A short cleanupGravatar Amin Timany2017-06-16
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
* Using UInfoInd for universes in inductive typesGravatar Amin Timany2017-06-16
* Extend definition of inductives to include subtyping infoGravatar Amin Timany2017-06-16
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of mod_bound_idGravatar ppedrot2012-12-18
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (kernel)Gravatar ppedrot2012-11-22
* More monomorphizationsGravatar ppedrot2012-11-13
* 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
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Noise for nothingGravatar pboutill2012-03-02
* Hash-consing of mutual_inductive_body (and Univ.constraints)Gravatar letouzey2011-10-10
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* Mod_subst: improving sharing of subst_mpsGravatar letouzey2011-02-24
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Mrec was not substituted correctlyGravatar barras2010-05-20
* Applicative commutative cuts in Fixpoint guard conditionGravatar pboutill2010-05-18
* Added a few informations about file lineages (for the most part in kernel)Gravatar herbelin2010-05-09
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
* Report des commits 11417 et 11437 de la v8.2Gravatar soubiran2008-10-15
* Ajout des alias de module dans le noyau.Gravatar soubiran2008-03-14
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* New keyword "Inline" for Parameters and Axioms for automatic Gravatar soubiran2007-04-25
* 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
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* - Correction bug calcul mind_consnrealargs, introduit à la révisionGravatar herbelin2006-03-22
* Documentation mutual_inductive_bodyGravatar herbelin2006-03-18
* Ajout de la longueur de l'arité des constructeurs dans one_inductive_body et...Gravatar herbelin2006-01-10
* Changement des named_contextGravatar gregoire2005-12-02
* Types inductifs parametriquesGravatar mohring2005-11-02
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 02:03:28 +0000