aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-11-26removal of CC.v lemata in cc (deprecated)corbinea
2003-11-26majfilliatr
2003-11-25Garder 'destruct using' a l'affichage ?herbelin
2003-11-25modif lexer: ident peut commencer par _barras
2003-11-25Version preliminaire pour la V8herbelin
2003-11-25Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...herbelin
2003-11-25Traduction Print Proofherbelin
2003-11-25CC: added injection theorycorbinea
2003-11-25textesmarche
2003-11-25majfilliatr
2003-11-25majfilliatr
2003-11-24aboutmarche
2003-11-24MAJherbelin
2003-11-24tentative de completion ESC-/ a la emacsletouzey
2003-11-24Prise en compte des defs syntaxiques dans is_global et global_reference qui p...herbelin
2003-11-24Renoncement de la compatibilite des noms qualifies au profit de la compatibil...herbelin
2003-11-24majfilliatr
2003-11-24majfilliatr
2003-11-23MAJherbelin
2003-11-23MAJsherbelin
2003-11-23Prise en compte des definitions locales dans les (co-)points-fixesherbelin
2003-11-22Compatibiliteherbelin
2003-11-22Traitement plus clair, notamment pour Locate, de quand quoter les composantes...herbelin
2003-11-22Bug introduit avec le 'Simpl f'herbelin
2003-11-22majfilliatr
2003-11-22majfilliatr
2003-11-21Suppression des niveaux videsherbelin
2003-11-21ajout Pnat et Pcompare_antisymherbelin
2003-11-21Ajout 'Simpl f'herbelin
2003-11-21Simplification; ajout Zcompare_antisymherbelin
2003-11-21ajout Pnat (suite)herbelin
2003-11-21ajout Pnat (suite)herbelin
2003-11-21Extraction des lemmes sur convert/nat_of_P de BinPos vers Pnat; ajout Pcase e...herbelin
2003-11-21Ajout Print Implicitherbelin
2003-11-21Tri et typoherbelin
2003-11-21MAJ format et docherbelin
2003-11-21Pas d'entrees autres que les predefinies en v8herbelin
2003-11-21majfilliatr
2003-11-20Nouvelle solution pour le probleme d'effacement des niveaux vides de opercons...herbelin
2003-11-20Code simplification in CCcorbinea
2003-11-20majfilliatr
2003-11-20majfilliatr
2003-11-19ajout de Znumtheory.v dans ZArithletouzey
2003-11-19Restauration compatibilite 7.4 pour le Hint Unfold Rgtherbelin
2003-11-19Prise en compte renommagesherbelin
2003-11-19Distinction entre 'as _' qui cache le terme filtre (si variable) et rien dans...herbelin
2003-11-19Deplacement subst_rawconstr dans Rawtermherbelin
2003-11-19Protection contre l'effacement des niveaux vides de operconstr et pattern par...herbelin
2003-11-19majfilliatr
2003-11-18correction suite ajout nouvelles tactiquesclrenard