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
*
Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized the
herbelin
2008-07-23
*
Nettoyage Wf.v et unification (suite remarques faites sur cocorico)
herbelin
2008-03-23
*
Do a second pass on the treatment of user-given implicit arguments. Now
msozeau
2008-03-15
*
still one more substituion s/Set/Type/
letouzey
2008-03-04
*
Proper implicit arguments handling for assumptions
msozeau
2008-02-26
*
repetition d'hypotheses dans well_founded_induction_type_2
letouzey
2006-06-25
*
Modification des propriétés (svn:executable)
notin
2006-03-17
*
Application des remarques de Pierre Casteran (A:Type plutôt que A:Set) et Ru...
herbelin
2006-02-06
*
Application de la suggestion de Nicolas Magaud (#1060)
herbelin
2006-01-22
*
Backtrack commit précédent: la préservation de l'énoncé exact Acc_ind es...
herbelin
2006-01-21
*
Préservation énoncé exact Acc_ind par choix nom 'a' comme paramètre de Acc
herbelin
2006-01-21
*
changement parametres inductifs dans les theories
mohring
2005-11-30
*
Documentation
herbelin
2005-05-19
*
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