aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cooking.mli
Commit message (Expand)AuthorAge
* Cooking.cook_constant: remove unused env argument.Gravatar Gaëtan Gilbert2018-07-03
* Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
* Getting rid of the const_proj field in the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
* Reduce circular dependency constants <-> projectionsGravatar Gaëtan Gilbert2018-05-31
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
* Using a record type for Cooking.result.Gravatar Pierre-Marie Pédrot2017-07-26
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Fix hashconsing of terms in the kernel.Gravatar Pierre-Marie Pédrot2017-03-27
* CLEANUP: Type alias "Context.section_context" was removedGravatar Matej Kosik2016-08-25
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* 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
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Minor cleanup around Term_typingGravatar letouzey2013-02-27
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of identifierGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* Proof using: nested sections bugfixGravatar gareuselesinge2012-06-18
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* 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
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Nouvelle en-têteGravatar herbelin2004-07-16
* Lazy manuelles dans le codeGravatar coq2002-10-07
* Lazy experimentale temporaire...Gravatar coq2002-10-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* repare la perte d'opacite a la fermeture de sectionGravatar barras2001-09-21
* Mécanisme pour faire remonter les contraintes de typage sur les variables de...Gravatar herbelin2001-09-09
* ParsingGravatar herbelin2001-08-10
* entetesGravatar filliatr2001-03-15
* Tables séparées pour chaque type de globalGravatar herbelin2000-11-20
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 09:24:56 +0000