aboutsummaryrefslogtreecommitdiff
path: root/pretyping/reductionops.ml
AgeCommit message (Expand)Author
2005-03-10A défaut de substitution paresseuse ou explicite, ajout d'une substitution o...herbelin
2005-02-18Ajout splay_lambdaherbelin
2004-09-17restructuration des printers: proofs passe avant parsingbarras
2004-09-15hiding the meta_map in evar_defsbarras
2004-09-03premiere reorganisation de l\'unificationbarras
2004-07-16Nouvelle en-têteherbelin
2004-06-29Essai de suppression de eta dans simpl (cf bug #779)herbelin
2004-05-14test de conversion laissait echapper exception NotConvertiblebarras
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-11-05Intégration des modifs de la branche mowgli :herbelin
2001-11-06corrections mineures suite au commit de restructuration du noyaubarras
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
2001-11-05GROS COMMIT:barras