index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
failure
Commit message (
Expand
)
Author
Age
*
Fixing critical inductive polymorphism bug found by Bruno.
herbelin
2011-10-05
*
Applying and reworking Tom Prince's patch for test-suite/failure/universes2.v
herbelin
2011-04-08
*
Fix inconsistency in Prop/Set conversion check
glondu
2010-09-23
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Added examples for checking that the guard condition excludes subterms
herbelin
2010-05-20
*
Fixed bug #2260 (check of resolution of all evars in the declaration
herbelin
2010-03-24
*
Improved the treatment of Local/Global options (noneffective Local on
herbelin
2009-10-25
*
Fixed a bug introduced in revision 12265.
herbelin
2009-10-08
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Relatively ad hoc fix to an ill-typed instantiation bug in type
herbelin
2009-08-11
*
fixed kernel bug (de Bruijn) + test-suite
barras
2008-12-02
*
added tests for hyps reordering
barras
2008-11-27
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
Correction d'une incohérence de typage des inductifs polymorphes: les
herbelin
2008-07-25
*
fixed universes bug related to module inclusion
barras
2008-04-22
*
test module include w.r.t. universe constraints
barras
2008-04-21
*
Vérification que "rewrite in" se comporte comme "rewrite" et échoue
herbelin
2007-10-16
*
Itération sur les sous-termes dans la vérification de la condition de garde
herbelin
2007-09-06
*
Fixed the pseudo-cicularity problem due to the with operator on Module Type.
soubiran
2007-02-21
*
Tests de référence circulaire au sous-typage de module (pour mémoire)
herbelin
2007-01-19
*
Correction bug #1302
herbelin
2007-01-17
*
test condition de garde
barras
2006-12-13
*
Check that sort-polymorphic inductive types is not too lax
herbelin
2006-10-27
*
Cette dérivation de paradoxe passait en V8.1beta
herbelin
2006-10-27
*
Adaptation des tests suite à la modification de Rewrite .. in (r9201)
notin
2006-10-13
*
+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no
jforest
2006-08-22
*
Stricte positivité en présence de types inductifs imbriqués avec paramètr...
herbelin
2006-06-23
*
Deux vérifications que le polymorphisme de sorte des inductifs ne fonctionne...
herbelin
2006-06-22
*
Correction trou de typage des éliminations d'inductifs introduit dans commit...
herbelin
2006-05-13
*
Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...
notin
2006-04-28
*
Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8
herbelin
2005-12-21
*
cf ltac4.v
herbelin
2005-12-21
*
deplacement params_ind
mohring
2005-11-03
*
test-suite/output/Notations.out
herbelin
2004-11-17
*
*** empty log message ***
herbelin
2004-10-17
*
Nouvelle en-tête
herbelin
2004-07-16
*
ajout test de non-regression Clear d'une def locale
barras
2003-12-17
*
Cacher les .v8
herbelin
2003-10-10
*
test d'implicite incorrect depuis que eq porte sur Type
barras
2003-09-23
*
*** empty log message ***
herbelin
2003-01-20
*
Tests ltac
herbelin
2003-01-19
*
Test for redundant clauses
herbelin
2002-08-15
*
Locate n'échoue plus: déplacement de Remark1 et Remark2 dans output
herbelin
2002-06-07
*
*** empty log message ***
herbelin
2002-04-12
*
*** empty log message ***
herbelin
2001-11-21
*
Sur l'exahustivité du filtrage
herbelin
2001-11-21
*
Test soumis par Randy Pollack
herbelin
2001-10-17
*
Test de dépendances de ClearBody
herbelin
2001-10-05
*
Quelques signes extérieurs de la sémantique de Remark, question visibilité
herbelin
2001-09-19
*
Tests l'incohérence des univers
herbelin
2001-09-09
[next]