aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cooking.ml
Commit message (Expand)AuthorAge
* Minor cleanup around Term_typingGravatar letouzey2013-02-27
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (kernel)Gravatar ppedrot2012-11-22
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Proof using: nested sections bugfixGravatar gareuselesinge2012-06-18
* Noise for nothingGravatar pboutill2012-03-02
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* 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
* 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
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Réutilisation de l'infrastructure pour le polymorphisme d'univers desGravatar herbelin2008-04-30
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* New keyword "Inline" for Parameters and Axioms for automatic Gravatar soubiran2007-04-25
* dependencesGravatar barras2006-10-30
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* 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
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* compat ocaml 3.03Gravatar filliatr2001-12-13
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* GROS COMMIT:Gravatar barras2001-11-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
* Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...Gravatar herbelin2001-07-21
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* entetesGravatar filliatr2001-03-15
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 05:06:08 +0000