aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
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
2003-11-02Protection contre les buts sans inegaliteherbelin
2003-11-01Ajout CPatNotation, PrintVisibilityherbelin
2003-11-01Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...herbelin
2003-10-30Redirected some of the verbose jprover output through the Pp module.corbinea
2003-10-30Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...herbelin
2003-10-30traduction des noms de correctnessherbelin
2003-10-28Ajout notations pour les expressions dans un anneauherbelin
2003-10-28Simplification preuveherbelin
2003-10-23Conjecture declare maintenant un axiome; reorganisation VernacDefinitionherbelin
2003-10-23Jprover bugfix (hopefully !)corbinea
2003-10-22Ajout NArithRingherbelin
2003-10-22Integration de SearchNamed dans SearchAboutherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:24:33 +0000