index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
theories
/
Lists
Age
Commit message (
Expand
)
Author
2006-04-28
Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...
notin
2006-04-06
versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmes
letouzey
2006-04-06
versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmes
letouzey
2006-03-17
Modification des propriétés (svn:executable)
notin
2006-03-16
propriete svn:keywords positionnee a Author Date Id Revision sur l'ensemble d...
letouzey
2006-03-16
utilisation de removeA dans FSetProperties
letouzey
2006-03-15
renommage NoRedun vers le plus joli NoDup
letouzey
2006-03-15
Typo
letouzey
2006-03-15
Typo
letouzey
2006-03-15
Ajout de fonctions sur les listes
notin
2006-03-15
Ajout de theories/FSets contenant la partie "light" de FSets et FMap:
letouzey
2006-02-22
MAJ
herbelin
2005-11-30
changement parametres inductifs dans les theories
mohring
2005-03-16
MAJ PolyList -> List
herbelin
2004-12-19
In_dec transparent (wish #902)
herbelin
2004-07-16
Nouvelle en-tête
herbelin
2004-03-28
Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...
herbelin
2003-12-24
Ajout delimiteur et arguments de scope pour list
herbelin
2003-12-15
modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes
barras
2003-11-29
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...
herbelin
2003-10-23
Commentaires
herbelin
2003-10-22
reorganisation des niveaux (ex: = est a 70)
barras
2003-10-15
Nettoyage argument de nil
herbelin
2003-10-10
MAJ commentaires
herbelin
2003-10-10
Renommage en v8 de PolyList en List et List en MonoList
herbelin
2003-10-10
Renommage en v8 de PolyList en List et List en MonoList
herbelin
2003-10-03
Cacher les .v8
herbelin
2003-09-26
Induction -> NewInduction; '++' pour app
herbelin
2003-09-24
Destruct/Induction -> NewDestruct/NewInduction
herbelin
2003-09-22
Implicits maintenant au courant pour l'affichage
herbelin
2003-09-21
Changement de la politique de V8only: V8only tout seul signifie
herbelin
2003-09-19
'::' est deja pris en V7
herbelin
2003-09-19
Ajout notation :: pour cons
herbelin
2003-04-10
Calcul automatique de l'implicite de nil pour que l'affichage sache le traiter
herbelin
2003-04-09
cast de nil
herbelin
2003-04-09
nil en implicite dans la v8
herbelin
2003-04-07
Cosmetique
herbelin
2003-03-12
*** empty log message ***
barras
2002-04-17
*** empty log message ***
werner
2002-04-17
Uniformisation (Qed/Save et Implicits Arguments)
herbelin
2002-03-13
Ajout de lemmes
mohring
2002-02-22
Doc + ajout fold_symmetric et nth_In
herbelin
2002-02-14
option -dump-glob pour coqdoc
filliatr
2001-11-03
interversion de deux Elim dans In_dec pour que la fonction extraite soit effi...
letouzey
2001-08-29
ajout option , Exc --> option, et lemmes dans les theories
mohring
2001-08-13
Rétablissement nom de section Map après résolution bugs surcharge de noms
herbelin
2001-08-05
Expérimentation de NewDestruct et parfois NewInduction
herbelin
2001-07-16
modif Map section
mohring
2001-04-20
Library doc adjustments (until page 140)
coq
2001-04-19
Ajout de fonctions proposees par Cuiht Alvarado
mohring
[prev]
[next]