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