index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
success
Commit message (
Expand
)
Author
Age
*
Check local definitions in context of inductive types
herbelin
2003-09-06
*
Projections
herbelin
2003-09-03
*
Added a test for Functional Induction.
courtieu
2003-06-21
*
Test backtracking
herbelin
2003-05-22
*
Nouveaux tests
herbelin
2003-05-21
*
Ce que Try récupère
herbelin
2003-04-27
*
indentation
herbelin
2003-03-29
*
fixing a typo in the new Funinv.v test in test-suite/success
courtieu
2003-02-28
*
Adding tests for the "functional induction" facility.
bertot
2003-02-27
*
MAJ pour Reg
desmettr
2003-01-28
*
*** empty log message ***
barras
2003-01-22
*
Il ne doit plus y avoir de preuves non terminées à la sortie du fichier
herbelin
2003-01-19
*
Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...
herbelin
2003-01-15
*
Require SplitAbsolu -> Require Rfunctions pour compatibilite avec la nouvelle...
desmettr
2002-12-12
*
MAJ sur MAJ
herbelin
2002-12-02
*
Remplacement de Syntactic Definition par Notation
herbelin
2002-12-02
*
Remplacement de Syntactic Definition par Notation
herbelin
2002-11-24
*
Test de la correction d'un bug soumis par Dachuan Yu
herbelin
2002-11-06
*
Omega échouait à effacer les hypothèses à contenu arithmétique lorsque c...
herbelin
2002-10-23
*
Parenthèses manquantes pour se conformer à la doc (et au nouveau PeanoSynta...
herbelin
2002-10-21
*
Adding the congruence closure tactics (CC and CCsolve).
corbinea
2002-10-01
*
Encore quelques rangements dans Nametab + petits trucs
coq
2002-09-27
*
*** empty log message ***
desmettr
2002-07-22
*
correction bugs Tauto
courant
2002-07-19
*
*** empty log message ***
desmettr
2002-07-18
*
*** empty log message ***
corbinea
2002-07-05
*
Added a new uncompleteness bug found in Tauto.
corbinea
2002-07-05
*
*** empty log message ***
herbelin
2002-06-14
*
Test de l'interprétation des fermetures de Match Context (2ème)
herbelin
2002-06-13
*
Test de l'interprétation des fermetures de Match Context
herbelin
2002-06-13
*
Tests pour la tactique Reg
desmettr
2002-06-11
*
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-05-29
*
*** empty log message ***
herbelin
2002-02-28
*
*** 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
*
MAJ Grammar
herbelin
2001-12-19
*
NatRing (2ème)
herbelin
2001-12-19
*
NatRing
herbelin
2001-12-19
[next]