index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Init
/
Wf.v
Commit message (
Expand
)
Author
Age
*
Nouvelle en-tête
herbelin
2004-07-16
*
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...
herbelin
2003-11-29
*
well_founded_induction de nouveau transparent
letouzey
2003-09-28
*
Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...
herbelin
2003-09-23
*
recursion bien fondee sur des pairs
filliatr
2003-07-08
*
Concentration des notations officielles dans Init/Notations; restructuration ...
herbelin
2003-05-21
*
Un principe light d'elimination de Acc, suivant les remarques de Yves Bertot
letouzey
2003-04-28
*
Activation des implicites pour la v8
herbelin
2003-04-09
*
*** empty log message ***
barras
2003-03-12
*
Uniformisation (Qed/Save et Implicits Arguments)
herbelin
2002-04-17
*
Uniformisation des theoremes dans Set et Type (def. de Acc_rect et
barras
2002-02-19
*
option -dump-glob pour coqdoc
filliatr
2002-02-14
*
MAJ des Id pour coqweb
herbelin
2002-01-09
*
Suppression d'Export redondants
herbelin
2001-11-14
*
Expérimentation de NewDestruct et parfois NewInduction
herbelin
2001-08-05
*
documentation automatique de la bibliothèque standard
filliatr
2001-04-11
*
entetes
filliatr
2001-03-15
*
fichiers prelude Coq
filliatr
1999-12-13