aboutsummaryrefslogtreecommitdiff
path: root/pretyping/cbv.ml
AgeCommit message (Expand)Author
2016-07-03closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Pierre Letouzey
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-04-29Fix incorrect cbv reduction of primitive projections. (Bug #4634)Guillaume Melquiond
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-10-15To stay closer to non-primitive projections, only unfold primitiveMatthieu Sozeau
2014-09-27Fix bug 3662 by actually reducing primitive projections in cbv/compute.Matthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2012-12-18Modulification of nameppedrot
2012-11-22Monomorphization (pretyping)ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-03-02Noise for nothingpboutill
2011-11-25avoid relying on weak invariant in cbv.mlbgregoir
2011-08-08Esubst: make types of substitutions & lifts privatepuech
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-04-21fixed CBV strategy: it was too eager on terms likebarras
2009-02-06pushed evar reduction in kernelbarras
2006-05-10correction bugs dans Cbv (beta n-aire)barras
2006-05-09subst. explicites avec vecteursbarras
2005-12-02Changement des named_contextgregoire
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-09-03premiere reorganisation de l\'unificationbarras
2004-07-16Nouvelle en-têteherbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-04-16simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...letouzey
2002-03-01Nouveau comportement: Delta ne s'applique pas aux variables liées par un letherbelin
2001-11-29nouvel algo de conversion plus uniformebarras
2001-11-05GROS COMMIT:barras
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-09-20Transparentbarras
2001-07-21Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...herbelin
2001-07-02Nettoyage/restructuration des ensembles d'indicateurs de réductionsherbelin
2001-05-03Changement de la structure des points fixesbarras
2001-03-15entetesfilliatr
2001-03-01nouvelle implantation de la reductionbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 18:16:20 +0000