aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
2003-12-24Parenthesage du terme pour accepter 'of' comme non identherbelin
2003-12-24La correction precedente a mis en evidence un defaut de l'utilisation de intr...herbelin
2003-12-23'of' restait par erreur mot-cle dans psyntax.ml4 en v8herbelin
2003-12-23Retablissement de GIntuition juste pour FSetsherbelin
2003-12-23*** empty log message ***barras
2003-12-23Renommages des hypotheses transformees car en raison des possibles dependance...herbelin
2003-12-15modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesbarras
2003-12-09cc updatecorbinea
2003-12-02error messages adjustementcorbinea
2003-12-01Nouvelle tactique EExistsclrenard
2003-11-29Obsolete, cf Funind.v dans test-suiteherbelin
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-11-29ground->firstorder, cc-> congruence, CC final commitcorbinea
2003-11-27Retour des _eq en v8herbelin
2003-11-26Remplacement de l'indicateur de date "@" par 'at'herbelin
2003-11-26just forgot something in previous commitcorbinea
2003-11-26removal of CC.v lemata in cc (deprecated)corbinea
2003-11-25Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...herbelin
2003-11-25CC: added injection theorycorbinea
2003-11-24Prise en compte des defs syntaxiques dans is_global et global_reference qui p...herbelin
2003-11-20Code simplification in CCcorbinea
2003-11-19Prise en compte renommagesherbelin
2003-11-18correction suite ajout nouvelles tactiquesclrenard
2003-11-15Ajout Print Implicit avec depliage du typeherbelin
2003-11-14Ordre standard pour l'associativiteherbelin
2003-11-14Correction chemin de Zherbelin
2003-11-13moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...barras
2003-11-13factorisation et generalisation des clausesbarras
2003-11-12Bug TacIdherbelin
2003-11-12Restructuration ZArithherbelin
2003-11-12Noms/énoncés plus canoniquesherbelin
2003-11-12petits changements de syntaxebarras
2003-11-12les modifs depuis la 7.4letouzey
2003-11-12TODOletouzey
2003-11-12Extraction Module M devient simplement Extraction Mletouzey
2003-11-10Suppression SearchNamed finalement redondant avec SearchAboutherbelin
2003-11-10le pb du <<.v vu comme module>> engendre maintenant une erreurletouzey
2003-11-10message informant de l'ecriture d'un fichier extraitletouzey
2003-11-10révision du traitement des axiomes non réalisésletouzey
2003-11-10essai d'extraction sous un moduleletouzey
2003-11-09factorisation de (recursive) libraryletouzey
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local defherbelin
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local defherbelin
2003-11-06Added Instantiate ... incorbinea
2003-11-05Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...herbelin
2003-11-05Renommage canonique d'un lemme redondantherbelin
2003-11-05Déport des lemmes de Omega de ZArith vers OmegaLemmasherbelin
2003-11-05Renommage canonique d'un lemme redondantherbelin
2003-11-04Extension de zarithherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 06:31:44 +0000