index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
ideal-features
Commit message (
Expand
)
Author
Age
*
Ensuring all .v files end with a newline to make "sed -i" work better on them.
Hugo Herbelin
2017-08-21
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Update headers.
Maxime Dénès
2015-01-12
*
Updating headers.
herbelin
2012-08-08
*
ZArith + other : favor the use of modern names instead of compat notations
letouzey
2012-07-05
*
Suppression fichier Case8.v redondant
herbelin
2011-11-16
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Moved Case3.v from ideal features to success (it works since 8.2).
herbelin
2010-04-17
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Add test-suite file related to discussion of syntax of implicit binders.
msozeau
2008-11-09
*
test-suite/ideal-features/{apply.v -> eapply_evar.v}
glondu
2008-11-02
*
- Fixed many "Theorem with" bugs.
herbelin
2008-10-27
*
Mise en place d'un algorithme d'inversion des contraintes de type lors
herbelin
2008-05-05
*
Quelques exemples à méditer sur le polymorphisme d'universe des inductifs
herbelin
2007-10-24
*
Pas de solution à court terme pour ce problème de complexité
herbelin
2007-01-28
*
Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8
herbelin
2005-12-21
*
Nouvelle en-tête
herbelin
2004-07-16
*
Ces fichiers repassent (y restait un bug dans l'inférence du prédicat)
herbelin
2001-10-03
*
Comportements peut-être souhaités mais en tout cas non officiellement pris ...
herbelin
2001-09-19