index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
cbv.ml
Commit message (
Expand
)
Author
Age
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
fixed CBV strategy: it was too eager on terms like
barras
2009-04-21
*
pushed evar reduction in kernel
barras
2009-02-06
*
correction bugs dans Cbv (beta n-aire)
barras
2006-05-10
*
subst. explicites avec vecteurs
barras
2006-05-09
*
Changement des named_context
gregoire
2005-12-02
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...
letouzey
2003-04-16
*
Nouveau comportement: Delta ne s'applique pas aux variables liées par un let
herbelin
2002-03-01
*
nouvel algo de conversion plus uniforme
barras
2001-11-29
*
GROS COMMIT:
barras
2001-11-05
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
Transparent
barras
2001-09-20
*
Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...
herbelin
2001-07-21
*
Nettoyage/restructuration des ensembles d'indicateurs de réductions
herbelin
2001-07-02
*
Changement de la structure des points fixes
barras
2001-05-03
*
entetes
filliatr
2001-03-15
*
nouvelle implantation de la reduction
barras
2001-03-01