aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/closure.ml
Commit message (Expand)AuthorAge
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Added eta-expansion in kernel, type inference and tactic unification,Gravatar herbelin2010-09-20
* ported r13340 to trunkGravatar barras2010-07-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
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* pushed evar reduction in kernelGravatar barras2009-02-06
* Add the ability to give a transparent_state for conversion, toGravatar msozeau2008-04-20
* fold travaille maintenant sur la forme beta-iota-zeta réduite duGravatar herbelin2008-03-10
* normalisation (by closure) was not performed under fixpointsGravatar barras2007-07-12
* Correction de deux cas où les types inductifs n'étaient pas comparésGravatar herbelin2006-10-05
* correction bugs dans Cbv (beta n-aire)Gravatar barras2006-05-10
* subst. explicites avec vecteursGravatar barras2006-05-09
* amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)Gravatar barras2006-05-05
* bug #1096: whd_stack on one arg of conversion had side-effect on the other argGravatar barras2006-05-03
* Changement des named_contextGravatar gregoire2005-12-02
* petites corrections + contournement bug projectionsGravatar barras2005-11-18
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* argument inutilisé de zip: toujours l'identitéGravatar letouzey2005-08-22
* reactivation de l optim des fermeturesGravatar barras2005-07-13
* backtrack modif de knh...Gravatar barras2005-07-13
* test du tag de reductionGravatar barras2005-07-12
* 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
* Ajout de l'opti des fermeture (mais debranche pour l'instant)Gravatar barras2003-08-06
* Improved reduction machine with closure: should use less memoryGravatar barras2003-08-05
* simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...Gravatar letouzey2003-04-16
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* pattern-matching avec cas inutilise dans closureGravatar barras2002-10-15
* Strengthenning rules for modules + No modules in sectionsGravatar coq2002-08-16
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* open Univ inutileGravatar courant2002-03-12
* cosmetiqueGravatar herbelin2002-01-30
* compat ocaml 3.03Gravatar filliatr2001-12-13
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
* 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
* TransparentGravatar barras2001-09-20
* Version de la reduction dans Closure plus econome en memoire:Gravatar barras2001-09-05
* NettoyageGravatar herbelin2001-07-21
* Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...Gravatar herbelin2001-07-21
* Nettoyage/restructuration des ensembles d'indicateurs de réductionsGravatar herbelin2001-07-02
* Changement de la structure des points fixesGravatar barras2001-05-03
* to_constr renvoie directement un constr pour contourner l'ancien Term.mk_cons...Gravatar herbelin2001-04-15