aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2001-10-03Correction messages d'erreurherbelin
2001-10-03Ces fichiers repassent (y restait un bug dans l'inférence du prédicat)herbelin
2001-10-03Tests de Cases avec définitions localesherbelin
2001-10-02Ajout de dynamiques pour les quotations constr et tacticdelahaye
2001-10-02Encapsulage des '<' et '>' pour éviter le regroupement '«'herbelin
2001-10-01correction de deux petits bugs: case_identité trop fort et Anomaly dans le t...letouzey
2001-10-01Incompatibilite camlp4 -pp et windows resolu a partir de camlp4 3.01.6herbelin
2001-10-01Il faut camlp4 > 3.01.6 pour windowsherbelin
2001-10-01Tests noms longs de modulesherbelin
2001-09-30Doc de Ltac, Field et AutoRewrite -> FAITdelahaye
2001-09-30Ajout du printer de tactiques + modif du Dynamic ocamldelahaye
2001-09-27Ultime Ultimeherbelin
2001-09-27Ajout INSTALL.winherbelin
2001-09-27Simplification de deux preuves. En outre ca simplifie leur extraction.letouzey
2001-09-27and_rec redondantletouzey
2001-09-26MAJ V7.1herbelin
2001-09-26Ultime MAJherbelin
2001-09-26tools pas fait automatiquementherbelin
2001-09-26Compatibilite Windoz/cygwinherbelin
2001-09-26Compatibilite Windowsherbelin
2001-09-26MAJ contribherbelin
2001-09-26Hack pour ajuster les chemins a la mode cygwinherbelin
2001-09-26Compatibilite Windozherbelin
2001-09-26Protection contre erreurs Unixherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-01 00:42:17 +0000