index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
Commit message (
Expand
)
Author
Age
...
*
I added a comment on the tactic compute_POS.
bertot
2002-06-07
*
This example does not work in coq-7.3, but does in coq-7.2.
bertot
2002-06-07
*
Ajout exemple JCF conflit variable interne, variable de section
herbelin
2002-06-06
*
Des exemples sérieux
herbelin
2002-06-06
*
Ajout exemple Yves renommage différent d'une var de section
herbelin
2002-06-06
*
Fusion entre la nouvelle et l'ancienne syntaxe de HintDestruct
herbelin
2002-06-05
*
*** empty log message ***
herbelin
2002-06-03
*
*** empty log message ***
herbelin
2002-05-29
*
Quelques bugs avec inject_nat
herbelin
2002-04-17
*
*** empty log message ***
herbelin
2002-04-12
*
*** empty log message ***
herbelin
2002-02-28
*
Test affichage O de nat dans une expression sur Z
herbelin
2002-01-25
*
*** empty log message ***
herbelin
2002-01-25
*
Ajout test de Pierre Crégut
herbelin
2002-01-21
*
*** empty log message ***
herbelin
2002-01-18
*
*** empty log message ***
herbelin
2002-01-18
*
Ajout d'un test sur les anonymes dépendant dans des arguments implicites
herbelin
2002-01-16
*
Test le filtrage dépendant vers l'avant
herbelin
2002-01-15
*
*** empty log message ***
herbelin
2001-12-21
*
Ajout d'un exemple de Christine
herbelin
2001-12-21
*
Test sobriété de la réduction de Intuition
herbelin
2001-12-19
*
Test sobriété de la réduction de Intuition
herbelin
2001-12-19
*
MAJ Grammar
herbelin
2001-12-19
*
NatRing (2ème)
herbelin
2001-12-19
*
NatRing
herbelin
2001-12-19
*
Un peu plus d'inférence des ? traitée par le Cases
herbelin
2001-12-19
*
*** empty log message ***
herbelin
2001-12-13
*
Test des coercions dans les motifs
herbelin
2001-12-11
*
*** empty log message ***
herbelin
2001-11-21
*
Possibilité d'appeler check avec l'option -byte
herbelin
2001-11-21
*
La synthèse des '?' dans l'exemple avec un let était un peu trop ambitieuse...
herbelin
2001-11-21
*
Un bug dans le script
herbelin
2001-11-21
*
Sur l'exahustivité du filtrage
herbelin
2001-11-21
*
Sur la cumulativité dans les tactiques
herbelin
2001-11-21
*
Nouveaux exemples
herbelin
2001-11-21
*
*** empty log message ***
herbelin
2001-11-20
*
*** empty log message ***
herbelin
2001-11-16
*
Quelques tests sur le let-in
herbelin
2001-11-08
*
Test syntaxe des constructions de l'état initial
herbelin
2001-10-17
*
Test soumis par Randy Pollack
herbelin
2001-10-17
*
Mise en place d'un test de correction de la sortie de commandes Coq
herbelin
2001-10-17
*
Commit par erreur
herbelin
2001-10-17
*
Test syntaxe des entiers relatifs
herbelin
2001-10-17
*
Test syntaxe des réels
herbelin
2001-10-17
*
*** empty log message ***
herbelin
2001-10-15
*
Test compatibilité V6 pour les filtrages avec let-in
herbelin
2001-10-15
*
Test de dépendances de ClearBody
herbelin
2001-10-05
*
Ces fichiers repassent (y restait un bug dans l'inférence du prédicat)
herbelin
2001-10-03
*
Tests de Cases avec définitions locales
herbelin
2001-10-03
*
Tests noms longs de modules
herbelin
2001-10-01
[prev]
[next]