index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
success
Age
Commit message (
Expand
)
Author
2004-03-26
*** empty log message ***
barras
2004-03-24
*** empty log message ***
barras
2004-03-24
bug de PP des fix (coqbugs #574)
barras
2004-03-13
Nouvel exemple; correction du contexte du précédent
herbelin
2004-03-12
Corrections
herbelin
2004-03-11
Test l'interprétation des scopes
herbelin
2004-03-11
Ajout exemple Inst
herbelin
2004-03-11
Ajout vieil exemple de coq-club
herbelin
2004-03-11
Ajout d'un vieil exemple de N. Magaud
herbelin
2004-03-11
Ajout bug #540
herbelin
2004-02-28
Exemple de Frederic
herbelin
2004-02-27
Ajout test synthese du predicat a partir du cast d'un filtrage avec dependances
herbelin
2004-02-09
New version of Functional Scheme and functional induction. Deals with
coq
2004-02-06
Test dependencies in constructors
herbelin
2004-02-06
Ajout filtrage sur motifs dépendants dans des inductifs différents
herbelin
2004-02-04
Vérification de la prise en compte des termes de type non inductif
herbelin
2003-12-27
Suppression en v8
herbelin
2003-12-24
BUG
herbelin
2003-12-23
Bug commit precedent
herbelin
2003-12-23
Renommages des hypotheses transformees car en raison des possibles dependance...
herbelin
2003-12-12
Ajout exemple Yves
herbelin
2003-12-05
Pour eviter d'avoir un gros type dans Set
herbelin
2003-11-29
ground->firstorder, cc-> congruence, CC final commit
corbinea
2003-11-26
removal of CC.v lemata in cc (deprecated)
corbinea
2003-11-25
CC: added injection theory
corbinea
2003-11-13
Niveau V8
herbelin
2003-11-13
Fermeture de la section maintenant necessaire
herbelin
2003-11-13
Passage a un SStream predicatif
herbelin
2003-11-09
Test Generalize
herbelin
2003-10-27
MAJ
herbelin
2003-10-14
Test obsolete
herbelin
2003-10-11
Logic_TypeSyntax disparu
herbelin
2003-10-10
Cacher les .v8
herbelin
2003-10-08
Teste interaction ltac et modules
herbelin
2003-10-08
Ajout exemple parametres implicites
herbelin
2003-10-08
Test Conjecture
herbelin
2003-10-07
Correction du bug 335 et Export/Require Export dans un module
coq
2003-09-23
Correction bug 328
coq
2003-09-06
Check local definitions in context of inductive types
herbelin
2003-09-03
Projections
herbelin
2003-06-21
Added a test for Functional Induction.
courtieu
2003-05-22
Test backtracking
herbelin
2003-05-21
Nouveaux tests
herbelin
2003-04-27
Ce que Try récupère
herbelin
2003-03-29
indentation
herbelin
2003-02-28
fixing a typo in the new Funinv.v test in test-suite/success
courtieu
2003-02-27
Adding tests for the "functional induction" facility.
bertot
2003-01-28
MAJ pour Reg
desmettr
2003-01-22
*** empty log message ***
barras
2003-01-19
Il ne doit plus y avoir de preuves non terminées à la sortie du fichier
herbelin
[next]