aboutsummaryrefslogtreecommitdiff
path: root/interp/reserve.ml
AgeCommit message (Expand)Author
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
2003-09-10Renommage des variables '_'herbelin
2003-09-09Ajout construction If primitive dans constr_expr et rawconstrherbelin
2003-08-11Ajout LetTupleherbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-03-29Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)herbelin