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
*
Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8
herbelin
2005-12-21
*
Abandon tests syntaxe v7; ajouts tests modules
herbelin
2005-12-21
*
MAJ syntaxe v7 avant activation en syntaxe v8
herbelin
2005-12-21
*
Activation du test de Refine en v7 pour mémoire avant passage à la v8
herbelin
2005-12-21
*
Anciennement déplacé dans 'output'
herbelin
2005-12-21
*
cf ltac4.v
herbelin
2005-12-21
*
L'option -no-vm laisse la place à une option -vm
herbelin
2005-12-18
*
*** empty log message ***
mohring
2005-11-03
*
deplacement params_ind
mohring
2005-11-03
*
Test reproductibilité du bug #1031
herbelin
2005-11-02
*
Ajout tests interactifs
herbelin
2005-11-02
*
Interactive test of Back
herbelin
2005-11-01
*
Declare Implicit Tactic
herbelin
2005-09-09
*
Suppression test CCSolve car remplaçé par Congruence mais qui ne traite pas...
herbelin
2005-09-09
*
Test clear final dans intros pattern
herbelin
2005-09-08
*
Consequence of allowing the numerical argument of auto to be an ident for ltac
herbelin
2005-05-23
*
A wish by Bas Spitters granted: a little more of unification up to
sacerdot
2005-05-19
*
Implemented autorewrite with ... in hyp [using ...].
sacerdot
2005-05-18
*
Ajout Unset Implicit Arguments manquant
herbelin
2005-03-21
*
Test d'un bug de 'Inv.dependent_hyps' qui ne met pas à jour le type des hyps...
herbelin
2005-03-20
*
Ajout test bug #935
herbelin
2005-03-19
*
Nouvelle syntaxe 'with' des modules non gérée en v7
herbelin
2005-03-17
*
Nouvelle syntaxe 'with' des modules non gérée en v7
herbelin
2005-03-16
*
Fix bug #931: leave dependent evars as such for refine
herbelin
2005-03-08
*
Suppression des fichiers temporaires
herbelin
2005-02-22
*
*** empty log message ***
herbelin
2005-02-21
*
Test bug #922
herbelin
2005-02-17
*
test de la bonne position des vars de ltac entre les vars et les rels
herbelin
2005-02-02
*
The new tutorial on (co)inductive types by Pierre Casteran.
sacerdot
2005-01-12
*
Ajout test bug 860
herbelin
2004-12-27
*
Réactivation des tests output avec test aussi de la nouvelle syntaxe
herbelin
2004-12-09
*
Ajout d'une version nouvelle syntaxe
herbelin
2004-12-09
*
MAJ avec les particularités de l'afficheur v7 de la V8
herbelin
2004-12-09
*
Test d'affichage d'un Fix donné avec /n
herbelin
2004-12-09
*
Fichier non traductible (référence à des objets invisibles ce qui empêche...
herbelin
2004-12-09
*
Intégré à Implicit.v
herbelin
2004-12-09
*
Ajout suffixe 8 pour test en nouvelle syntaxe
herbelin
2004-12-09
*
Plus de statut spécial pour Remark
herbelin
2004-12-09
*
Désactivation du test du printer arithmétique v7
herbelin
2004-12-09
*
Ajout bug do_restrict_hyp
herbelin
2004-12-08
*
Erreur commit précédent
herbelin
2004-12-06
*
Ajout bug #888
herbelin
2004-12-06
*
Ajout bug #889
herbelin
2004-12-06
*
Failed in 8.0pl1
herbelin
2004-12-04
*
Was failing in 8.0pl1
herbelin
2004-12-03
*
Suppression bruit perl
herbelin
2004-11-28
*
Re-commit version nouvelle syntaxe
herbelin
2004-11-28
*
Passage à la v8 pour test parser
herbelin
2004-11-28
*
Test lieurs dans Notation
herbelin
2004-11-17
*
test-suite/output/Notations.out
herbelin
2004-11-17
[next]