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