aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Suite unification apply et eapply (l'un et l'autre profite maintenantGravatar herbelin2007-04-16
* Essai de partage de code entre apply et eapplyGravatar herbelin2007-04-15
* Ajout d'un test de complexité de injection (cf bug 1173)Gravatar herbelin2007-04-14
* Suite du commit 9760 : l'uniformisation du comportement de one_step_reduce,Gravatar herbelin2007-04-14
* Correction bug #1499Gravatar notin2007-04-13
* Proposition de correction pour le bug #1173 (ou du moins pour unGravatar herbelin2007-04-13
* Correction bug #1477 sur ordre des variables partagées par les or-patterns.Gravatar herbelin2007-04-13
* Test non régression bug #1491Gravatar herbelin2007-04-13
* Correction bug #1491Gravatar herbelin2007-04-13
* Nettoyage des tactiques basées sur "simpl" (delta-réduction cachantGravatar herbelin2007-04-13
* Transparency of Z_lt_le_decGravatar notin2007-04-12
* Cleaned doc/common/title.tex file. Increased the space under headersGravatar emakarov2007-04-12
* Standardisation format biblioGravatar herbelin2007-04-12
* Nouveau déplacement de constr, cette fois au niveau 8. En fait, il y aGravatar herbelin2007-04-11
* Remontée de constr de 1 à 5 (pour permettre des notations entre 1 et 5Gravatar herbelin2007-04-10
* Some changes to eliminate Hevea warnings.Gravatar emakarov2007-04-10
* Split refman/headers.tex into headers.sty and headers.hva.Gravatar emakarov2007-04-10
* Eliminated warning messages from Hevea. Most warning messages wereGravatar emakarov2007-04-10
* simplier version of tail_plusGravatar letouzey2007-04-06
* Mise en place d'un rafinement de compute. Gravatar jforest2007-04-05
* On n'a plus besoin de compiler les anciens fichiers de functionnal induction ...Gravatar jforest2007-04-05
* Correction partielle du bug #1388 (augmentation de la taille des code accepte...Gravatar jforest2007-04-05
* Mise en place d'une nouvelle strategie plus efficace pour les preuves de Func...Gravatar jforest2007-04-05
* Corrected a typo in doc/refman/Setoid.tex.Gravatar emakarov2007-04-04
* Added back the tactics [apply -> ident], etc. to Tactics.v afterGravatar emakarov2007-04-02
* Extension to the general sequence operator (tactical). Now in addition to ...Gravatar emakarov2007-04-02
* Intégration de la modification suggérée par Michal Moskal (cf msg sur Coq ...Gravatar notin2007-04-02
* Réparation de NArith/BinPos.v suite au commit #9739Gravatar notin2007-04-02
* Removed the definition of extensions of apply to equivalencesGravatar emakarov2007-04-01
* Added the following theorems to BinPos:Gravatar emakarov2007-03-30
* Added new tactics for applying equivalences (iff) to Tactics.v:Gravatar emakarov2007-03-30
* Modifications dans Makefile: Gravatar notin2007-03-30
* Changement mineur du comportement de 'rewrite .. in * |-': si leGravatar notin2007-03-30
* Support for implicit formal argument types in Program ; parse types in type s...Gravatar msozeau2007-03-28
* Modification de la vm:Gravatar notin2007-03-27
* Make multiple patterns work again with Program while simplifying the code.Gravatar msozeau2007-03-26
* stupid me: ?f two times in a patternGravatar letouzey2007-03-26
* PositiveOrderedTypeBits is now formulated to be a UsualOrderedType, not only ...Gravatar letouzey2007-03-26
* Correction des bugs #1455 et #1456Gravatar notin2007-03-22
* Remove debugging code committed by accidentGravatar lmamane2007-03-22
* A tentative fix for bug #1455Gravatar lmamane2007-03-22
* Suppression des sauts de lignes superflus de Show Script (test-suite/output/T...Gravatar notin2007-03-21
* Correction bug affichage des notations des noms de fonctions appliquéesGravatar herbelin2007-03-20
* Some tactic fixes in Subtac, fix obvious bug in admit_obligations but still a...Gravatar msozeau2007-03-20
* ajout contrib/dp/Dp.voGravatar filliatr2007-03-20
* traces ErgoGravatar filliatr2007-03-20
* Forgot to update to new castGravatar msozeau2007-03-19
* Add a parameter to QuestionMark evar kind to say it can be turned into an obl...Gravatar msozeau2007-03-19
* Un chouia de portabilité en plus et pas de test si pas de bogomipsGravatar herbelin2007-03-19
* MAJ test complexité pour considérer le cas d'un temps avec un nombreGravatar herbelin2007-03-17