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
*
'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
*
Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...
herbelin
2003-09-21
*
Nettoyage
herbelin
2003-09-21
*
'::' est deja pris en V7
herbelin
2003-09-19
*
Section et report Infix hors section
herbelin
2003-09-19
*
Plus besoin de V7only [ Import ... ] pour l'affichage des notations par le tr...
herbelin
2003-09-19
*
Ajout notation :: pour cons
herbelin
2003-09-19
*
Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem...
herbelin
2003-09-19
*
Suppression DatatypesSyntax et PeanoSyntax qui était vides
herbelin
2003-09-12
*
Ajout et MAJ commandes de scopes
herbelin
2003-09-12
*
Bind et Delimit pour R
herbelin
2003-09-12
*
Bind et Delimit pour nat
herbelin
2003-09-12
*
Bind et Delimit pour positive et Z (hors section)
herbelin
2003-09-12
*
Bind et Delimit pour R
herbelin
2003-09-12
*
Suppression notations redondantes en v8 : Fst, ProjS1, Value, Ex ...
herbelin
2003-09-11
*
principes de récurrences plus efficaces pour l'extraction
letouzey
2003-09-05
*
Zdiv plus efficace: r+r -> 2*r
letouzey
2003-09-05
*
Zabs_Zsgn
letouzey
2003-09-05
*
Passage de 'relation' à Type
herbelin
2003-09-01
*
Affichage {}+{}, niveau paire au plus haut
herbelin
2003-08-10
*
Un peu d'aide pour le traducteur
herbelin
2003-08-10
*
Coq.Init.Logic.eq au lieu de eq
filliatr
2003-07-18
*
recursion bien fondee sur des pairs
filliatr
2003-07-08
*
suppression de FSets (redevient une contrib)
filliatr
2003-06-24
*
doc
filliatr
2003-06-24
*
concat; debut split
filliatr
2003-06-24
*
join
filliatr
2003-06-23
*
add_tree : sur type tree plutot que sur type t
filliatr
2003-06-23
*
merge_bis et debug join
filliatr
2003-06-23
*
remov
filliatr
2003-06-20
*
merge
filliatr
2003-06-20
*
remove_min, remove_max
filliatr
2003-06-20
[next]