aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cbv.ml
Commit message (Expand)AuthorAge
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Modulification of nameGravatar ppedrot2012-12-18
* Monomorphization (pretyping)Gravatar ppedrot2012-11-22
* 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
* avoid relying on weak invariant in cbv.mlGravatar bgregoir2011-11-25
* Esubst: make types of substitutions & lifts privateGravatar puech2011-08-08
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* 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
* fixed CBV strategy: it was too eager on terms likeGravatar barras2009-04-21
* pushed evar reduction in kernelGravatar barras2009-02-06
* correction bugs dans Cbv (beta n-aire)Gravatar barras2006-05-10
* subst. explicites avec vecteursGravatar barras2006-05-09
* Changement des named_contextGravatar gregoire2005-12-02
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...Gravatar letouzey2003-04-16
* Nouveau comportement: Delta ne s'applique pas aux variables liées par un letGravatar herbelin2002-03-01
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* TransparentGravatar barras2001-09-20
* 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
* entetesGravatar filliatr2001-03-15
* nouvelle implantation de la reductionGravatar barras2001-03-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 20:47:33 +0000