index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
output
Commit message (
Expand
)
Author
Age
*
Ajout test notation récursive
herbelin
2006-01-11
*
Test choix conflit afficheur de nombres selon la présence ou pas d'une coercion
herbelin
2006-01-05
*
Affichage de 'O' (lettre) comme '0' (chiffre)
herbelin
2006-01-02
*
Test printing of Tactic Notation which was broken until dec 2005
herbelin
2005-12-23
*
Abandon tests syntaxe v7 (correction)
herbelin
2005-12-22
*
Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8
herbelin
2005-12-22
*
Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8
herbelin
2005-12-21
*
Nouvelle syntaxe 'with' des modules non gérée en v7
herbelin
2005-03-16
*
Ajout test bug 860
herbelin
2004-12-27
*
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
*
Test lieurs dans Notation
herbelin
2004-11-17
*
test-suite/output/Notations.out
herbelin
2004-11-17
*
Ajout tests affichage coercions vers Funclass
herbelin
2004-06-02
*
modif des fixpoints pour que si on donne une notation au produit, les pts fix...
barras
2004-03-05
*
*** empty log message ***
herbelin
2003-10-10
*
Correction du bug 335 et Export/Require Export dans un module
coq
2003-10-07
*
*** empty log message ***
barras
2003-03-14
*
MAJ
herbelin
2003-03-04
*
Pb de parenthèse dans "Check (S (plus O O))"
herbelin
2003-01-30
*
Il ne doit plus y avoir de preuves non terminées à la sortie du fichier
herbelin
2003-01-19
*
*** empty log message ***
herbelin
2003-01-16
*
Problème de désynchronisation des variables du type et du corps d'un point-...
herbelin
2003-01-15
*
Export M + Module M <: SIG
coq
2003-01-09
*
MAJ
herbelin
2002-11-25
*
MAJ
herbelin
2002-11-24
*
Des critères plus fins d'analyse des implicites automatiques; meilleur affic...
herbelin
2002-10-29
*
Parseur pour n>20 dans nat plus disponible
herbelin
2002-10-16
*
Encore quelques rangements dans Nametab + petits trucs
coq
2002-09-27
*
Changement de sémantique de Remark : maintenant un global comme les autres
herbelin
2002-09-21
*
Correction
coq
2002-08-21
*
Test affichage optimal des coercions
herbelin
2002-08-14
*
Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulement
filliatr
2002-06-21
*
Locate n'échoue plus: déplacement de Remark1 et Remark2 dans output
herbelin
2002-06-07
*
*** empty log message ***
herbelin
2002-06-03
*
*** empty log message ***
herbelin
2002-05-29
*
Quelques bugs avec inject_nat
herbelin
2002-04-17
*
Test affichage O de nat dans une expression sur Z
herbelin
2002-01-25
*
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
*
Test syntaxe des constructions de l'état initial
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