index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
Commit message (
Expand
)
Author
Age
...
*
lettac -> set
barras
2003-10-16
*
Syntax error
herbelin
2003-10-16
*
Suppression des surcharge de regles de grammaire en v7
herbelin
2003-10-16
*
Pour eviter des regles redondantes en v7
herbelin
2003-10-16
*
FTC_P2 maintenant dans RIneq
herbelin
2003-10-16
*
Ajout de quelques lemmes cles
herbelin
2003-10-16
*
Affichage = au lieu de == en v7
herbelin
2003-10-15
*
Nettoyage argument de nil
herbelin
2003-10-15
*
Changement 'as notation' en 'where notation'
herbelin
2003-10-14
*
Argument de except, error implicite seulement en v8; Changement 'as notation'...
herbelin
2003-10-14
*
Argument de None implicite seulement en v8
herbelin
2003-10-14
*
Argument implicite pour None, error, except
herbelin
2003-10-13
*
Notations pour l'exponentiation
herbelin
2003-10-13
*
Enregistrement '^' en v8
herbelin
2003-10-13
*
mise a jour nouvelle syntaxe
barras
2003-10-11
*
nat_scope ouvert par defaut
herbelin
2003-10-10
*
identity est equivalent sur Type (sauf sans argument)
herbelin
2003-10-10
*
type_scope
herbelin
2003-10-10
*
Suppression de definitions equivalentes
herbelin
2003-10-10
*
Notation '^'
herbelin
2003-10-10
*
Plus d'Eval Compute
herbelin
2003-10-10
*
MAJ commentaires
herbelin
2003-10-10
*
Delimiters N devient 'nat'
herbelin
2003-10-10
*
changement nouvelle syntaxe (pt fixes)
barras
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-10
*
Cacher les .v8
herbelin
2003-10-03
*
Retour sur la version non optimisee de 'add' pour compatibilite; renommage Un...
herbelin
2003-10-01
*
'_ = _ = _' maintenant predefini, meme en V7
herbelin
2003-09-30
*
une induction de moins dans lt_eq_lt_dec
letouzey
2003-09-28
*
well_founded_induction de nouveau transparent
letouzey
2003-09-28
*
'Open Local Scope' en attendant que le core_scope sache se mettre devant impl...
herbelin
2003-09-26
*
Induction -> NewInduction; '++' pour app
herbelin
2003-09-26
*
Passage de Destruct a NewDestruct; '-' pour negb
herbelin
2003-09-26
*
Structuration de fast_integer en operations sur positive, proprietes des oper...
herbelin
2003-09-26
*
add_x_x de fast_integer vers auxiliary
herbelin
2003-09-25
*
Retour provisoire a une section
herbelin
2003-09-25
*
Suppression section, ce qui evite de repliquer les declarations d'Infix
herbelin
2003-09-24
*
Destruct/Induction -> NewDestruct/NewInduction
herbelin
2003-09-24
*
Destruct -> NewDestruct
herbelin
2003-09-24
*
Remplacement de Induction/Destruct par NewInduction/NewDestruct
herbelin
2003-09-23
*
Remplacement de Induction/Destruct par NewInduction/NewDestruct
herbelin
2003-09-23
*
Remplacement de Induction/Destruct par NewInduction/NewDestruct
herbelin
2003-09-23
*
Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...
herbelin
2003-09-23
*
traducteur: affiche les commentaires a l'interieur des commandes
barras
2003-09-22
*
Implicits maintenant au courant pour l'affichage
herbelin
2003-09-22
*
Deplacement de lemmes de IntMap vers ZArith
herbelin
2003-09-22
*
Changement de la politique de V8only: V8only tout seul signifie
herbelin
2003-09-21
*
Conflit de nom Pplus dans positive et dans polynomial (de ring)
herbelin
2003-09-21
*
Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...
herbelin
2003-09-21
[prev]
[next]