aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2001-10-30legeres modifs pretty-print de l'extractionsletouzey
2001-10-30Reorganisation de Goption. Passage des options l'utilisant en synchroneletouzey
2001-10-29Amérioration message d'erreur en cas d'échec du filtrage de premier ordreherbelin
2001-10-29Oups: un relicat de fn de cacheletouzey
2001-10-26Vérification précoce qu'un lemme n'existe pas déjàherbelin
2001-10-26Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ET...letouzey
2001-10-25correctif bug des de Bruijn du Double Caseletouzey
2001-10-24Suppression de Logic_Type.sigT, redondant avec Specif.sigTherbelin
2001-10-24seisme suite. correction bugsletouzey
2001-10-24Patch de goption.ml pour faire marcher les options synchrones. Passage des op...letouzey
2001-10-23Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRdelahaye
2001-10-23suite du seismeletouzey
2001-10-23Bug Induction (prise en compte let-in + ordre des dépendances dans thin)herbelin
2001-10-22chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les o...letouzey
2001-10-17Test syntaxe des constructions de l'état initialherbelin
2001-10-17Test soumis par Randy Pollackherbelin
2001-10-17Mise en place d'un test de correction de la sortie de commandes Coqherbelin
2001-10-17Commit par erreurherbelin
2001-10-17Test syntaxe des entiers relatifsherbelin
2001-10-17Test syntaxe des réelsherbelin
2001-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre se...herbelin
2001-10-17Nouvelle fonctionherbelin
2001-10-17Amélioration mise en page Print ML Module et Print ML Moduleherbelin
2001-10-16MAJherbelin
2001-10-16Nettoyage Recordobj et conséquencesherbelin
2001-10-15*** empty log message ***herbelin
2001-10-15Test compatibilité V6 pour les filtrages avec let-inherbelin
2001-10-15Export hide_ident_or_numarg_tacticherbelin
2001-10-15Insertion automatique des motifs de let-in s'il ne sont pas explicitement men...herbelin
2001-10-15Rustine pour rendre les messages d'erreurs de la compilation des Cases plus l...herbelin
2001-10-15Prise en compte Intros until dans Discriminate, Injection et Simplify_eq + ne...herbelin
2001-10-15Nouvelle correction du bug confusion entre implicites de locaux et de globauxherbelin
2001-10-15Insertion automatique des motifs de let-in s'il ne sont pas explicitement men...herbelin
2001-10-15Orthographeherbelin
2001-10-12Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...herbelin
2001-10-12MAJherbelin
2001-10-12reparationfilliatr
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
2001-10-11Bug collision entre les implicites d'un global et les variables locales de mÃ...herbelin
2001-10-10Incompatibilité entre la prise en compte des univers au niveau des tactiques...herbelin
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-10-05Petit oubli à propos de ThinBodyherbelin
2001-10-05Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...herbelin
2001-10-05un echo de débogage superfluherbelin
2001-10-05Test de dépendances de ClearBodyherbelin
2001-10-03Bug de synthèse du prédicat en présence d'arguments non filtrable; correct...herbelin
2001-10-03Bug d'affichage du prédicat, bug d'affichage des clauses en présence de dé...herbelin
2001-10-03Bugs de vérification de la bonne fondation en présence de définitions loca...herbelin
2001-10-03coqtop includes itself the needed pathsherbelin
2001-10-03MAJ docherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 23:16:45 +0000