Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Passage de lconstr à constr pour les arguments immédiat de commandes | herbelin | 2003-09-06 |
* | Pb de mot-cle | herbelin | 2003-08-14 |
* | Nouvelle mouture du traducteur v7->v8 | herbelin | 2003-08-11 |
* | Bug compilation | herbelin | 2003-06-20 |
* | Ajout 'Symmetry in Hyp'; chgt syntaxe 'change ... with ...' | herbelin | 2003-06-19 |
* | Utilisation de intro_pattern dans NewDestruct/NewInduction | herbelin | 2003-06-13 |
* | Suppression définitive de lmatch et or_metanum dans tacinterp | herbelin | 2003-05-21 |
* | Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ... | herbelin | 2003-05-21 |
* | Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern | herbelin | 2003-05-19 |
* | Factorisation des produits de même type; parenthèses autour des x:=c et n:=... | herbelin | 2003-04-29 |
* | Globalisation des noms de tactiques dans les définitions de tactiques | herbelin | 2003-04-07 |
* | Bug pattern_occ_hyp_list | herbelin | 2003-03-31 |
* | *** empty log message *** | barras | 2003-03-12 |