index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
theories
Age
Commit message (
Expand
)
Author
2003-09-12
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-11
Suppression notations redondantes en v8 : Fst, ProjS1, Value, Ex ...
herbelin
2003-09-05
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-01
Passage de 'relation' à Type
herbelin
2003-08-10
Affichage {}+{}, niveau paire au plus haut
herbelin
2003-08-10
Un peu d'aide pour le traducteur
herbelin
2003-07-18
Coq.Init.Logic.eq au lieu de eq
filliatr
2003-07-08
recursion bien fondee sur des pairs
filliatr
2003-06-24
suppression de FSets (redevient une contrib)
filliatr
2003-06-24
doc
filliatr
2003-06-24
concat; debut split
filliatr
2003-06-23
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-20
remov
filliatr
2003-06-20
merge
filliatr
2003-06-20
remove_min, remove_max
filliatr
2003-06-19
add
filliatr
2003-06-19
bal: preuve terminee
filliatr
2003-06-19
bal: premier cas hl > hr + 2
filliatr
2003-06-19
typo
filliatr
2003-06-18
AVL: suite
filliatr
2003-06-18
Arguments superflus pour Zlength_nil
herbelin
2003-06-17
AVL: suite
filliatr
2003-06-17
AVL de caml: un debut
filliatr
2003-06-16
Ground depth
filliatr
2003-06-16
reparation fsets suite a changement de Ground
filliatr
2003-06-14
Deplacement de le_minus de fast_integer vers Minus
herbelin
2003-06-14
Deplacement de le_minus de fast_integer vers Minus
herbelin
2003-06-13
changement de spécif du fold
letouzey
2003-06-13
fcts tail-recursives
filliatr
2003-06-13
Require Export
filliatr
2003-06-13
FSets, mais pas compile' par make world
filliatr
2003-06-13
suite changements ZArith en vu de librairie FSet
letouzey
2003-06-13
quelques adaptations de Zarith en vu de la nouvelle librarie FSet
letouzey
2003-06-13
Deplacement d'un lemme sur nat de ZArith vers Arith
herbelin
2003-06-12
INZ reste constante pour compat V7 mais Unfold INZ est supprimé par le tradu...
herbelin
2003-06-10
Import nat_scope
herbelin
2003-06-10
Suppression d'une occurrence superflue d'argument de type dans Notation sacha...
herbelin
2003-06-10
Deplacement delimiteur T dans Notations
herbelin
2003-05-29
Bug niveau
herbelin
2003-05-29
niveau 49 devient next
herbelin
2003-05-29
niveau 49 devient next
herbelin
[next]