aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2007-04-05Correction partielle du bug #1388 (augmentation de la taille des code accepte...jforest
2007-04-05Mise en place d'une nouvelle strategie plus efficace pour les preuves de Func...jforest
2007-04-04Corrected a typo in doc/refman/Setoid.tex.emakarov
2007-04-02Added back the tactics [apply -> ident], etc. to Tactics.v afteremakarov
2007-04-02Extension to the general sequence operator (tactical). Now in addition to ...emakarov
2007-04-02Intégration de la modification suggérée par Michal Moskal (cf msg sur Coq ...notin
2007-04-02Réparation de NArith/BinPos.v suite au commit #9739notin
2007-04-01Removed the definition of extensions of apply to equivalencesemakarov
2007-03-30Added the following theorems to BinPos:emakarov
2007-03-30Added new tactics for applying equivalences (iff) to Tactics.v:emakarov
2007-03-30Modifications dans Makefile: notin
2007-03-30Changement mineur du comportement de 'rewrite .. in * |-': si lenotin
2007-03-28Support for implicit formal argument types in Program ; parse types in type s...msozeau
2007-03-27Modification de la vm:notin
2007-03-26Make multiple patterns work again with Program while simplifying the code.msozeau
2007-03-26stupid me: ?f two times in a patternletouzey
2007-03-26PositiveOrderedTypeBits is now formulated to be a UsualOrderedType, not only ...letouzey
2007-03-22Correction des bugs #1455 et #1456notin
2007-03-22Remove debugging code committed by accidentlmamane
2007-03-22A tentative fix for bug #1455lmamane
2007-03-21Suppression des sauts de lignes superflus de Show Script (test-suite/output/T...notin
2007-03-20Correction bug affichage des notations des noms de fonctions appliquéesherbelin
2007-03-20Some tactic fixes in Subtac, fix obvious bug in admit_obligations but still a...msozeau
2007-03-20ajout contrib/dp/Dp.vofilliatr
2007-03-20traces Ergofilliatr
2007-03-19Forgot to update to new castmsozeau
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an obl...msozeau
2007-03-19Un chouia de portabilité en plus et pas de test si pas de bogomipsherbelin
2007-03-17MAJ test complexité pour considérer le cas d'un temps avec un nombreherbelin
2007-03-16Correction du bug #1441notin
2007-03-16 r11153@tannat: jforest | 2007-03-16 10:25:55 +0100jforest
2007-03-15Test de non-régression pour commit 9673herbelin
2007-03-15Typosherbelin
2007-03-15Suppression argument pattern_source du case_info (code jamais utilisé)herbelin
2007-03-15Prévention notations récursives sans terminal à gauche et qui font bouclerherbelin
2007-03-15Add destruct_call variant where naming of introduced hypotheses is possible. ...msozeau
2007-03-14Add destruct_call_concl in SubtacTactics and fix obvious obligation handling ...msozeau
2007-03-14Bug dans Makefile (COQINSTALLPREFIX)notin
2007-03-14Removed an unnecessary argument (p : positive) in Prect_base.emakarov
2007-03-13Solve obligation handling bug of trying to solve automatically at Next Obliga...msozeau
2007-03-13Correction bug #1439 (comportement de replace by)notin
2007-03-12Proof simplification for eq_nat_dec et le_lt_dec: induction over letouzey
2007-03-11correction du bug 1432jforest
2007-03-11Remove bugguy notationsmsozeau
2007-03-09bug#1434 importing fonctor arguments, now it works.soubiran
2007-03-08Create a program_scope in subtac Utilsmsozeau
2007-03-08Add Program keywords to coqwcmsozeau
2007-03-08Transparence de eq_dec et lt_dec daans OrderedTypeFactsnotin
2007-03-07Application suggestion #1430 de Yevgeniy pour TEXINPUTSherbelin
2007-03-06màj dépendances .v: SubtacTactics.volmamane
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 01:35:55 +0000