index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
ZArith
/
Wf_Z.v
Commit message (
Expand
)
Author
Age
*
Finalement, préservation de la compatibilité pour Z_lt_induction et ajout p...
herbelin
2005-05-02
*
Fixed hypotheses of Z_lt_induction (see #957)
herbelin
2005-04-26
*
Nouvelle en-tête
herbelin
2004-07-16
*
changement de pose en set (pose n'etait pas utilise avec la semantique
barras
2003-12-24
*
modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes
barras
2003-12-15
*
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...
herbelin
2003-11-29
*
ground->firstorder, cc-> congruence, CC final commit
corbinea
2003-11-29
*
Deplacement ZERO_le_inj dans Zorder
herbelin
2003-11-18
*
Ajout lemmes; independance vis a vis noms variables liees
herbelin
2003-11-12
*
Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de...
herbelin
2003-11-05
*
principes de récurrences plus efficaces pour l'extraction
letouzey
2003-09-05
*
recursion bien fondee sur des pairs
filliatr
2003-07-08
*
FSets, mais pas compile' par make world
filliatr
2003-06-13
*
quelques adaptations de Zarith en vu de la nouvelle librarie FSet
letouzey
2003-06-13
*
Ajout Open Scope
herbelin
2003-04-09
*
Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".
herbelin
2003-04-09
*
*** empty log message ***
barras
2003-03-12
*
Uniformisation (Qed/Save et Implicits Arguments)
herbelin
2002-04-17
*
option -dump-glob pour coqdoc
filliatr
2002-02-14
*
ajouts provenant de Chinese dans ZArith + deplacements de 3 fichiers de contr...
letouzey
2002-01-18
*
Expérimentation de NewDestruct et parfois NewInduction
herbelin
2001-08-05
*
Library doc adjustments (until page 140)
coq
2001-04-20
*
remplace Zarith par ZArith
mohring
2001-04-19