index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
"subst." works now even when it exists an hypothesis have the form "x=x" in t...
jforest
2006-05-20
*
suite tentative pour permettre l'utilisation de modules de FSets
letouzey
2006-05-20
*
on cache autant que possible Raw dans FSet(Weak)List.Make
letouzey
2006-05-19
*
tests de Romega
letouzey
2006-05-19
*
Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort
herbelin
2006-05-19
*
ajout de mes modifs recentes
letouzey
2006-05-18
*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8829 85f007b7-540e-04...
letouzey
2006-05-18
*
Dépendances pour List.v
notin
2006-05-18
*
Correcting a bug in matching context on if.
jforest
2006-05-17
*
Typo dans List.v
notin
2006-05-17
*
updating Function documentation
jforest
2006-05-17
*
Ajout de [count_occ] dans List.v
notin
2006-05-17
*
etoffage des notions de permutations (a la fois List.Permutation et Permutati...
letouzey
2006-05-16
*
Typo dans CREDITS
notin
2006-05-16
*
ajout de theories/FSets/DecidableTypeEx.v
letouzey
2006-05-15
*
3*rien
letouzey
2006-05-15
*
ajout d'exemples de decidable types
letouzey
2006-05-15
*
petit ajout concernant InA
letouzey
2006-05-15
*
On remet plutot l'ancien nom Zgcd_is_pos au lieu de Zgcd_pos
letouzey
2006-05-14
*
In_dec de nouveau transparent
letouzey
2006-05-14
*
reparartion d'un petit oubli cassant PrecedenceGraph
letouzey
2006-05-14
*
typo
letouzey
2006-05-13
*
un Zgcd calculant dans coq
letouzey
2006-05-13
*
Code mort
herbelin
2006-05-13
*
Correction trou de typage des éliminations d'inductifs introduit dans commit...
herbelin
2006-05-13
*
correction bugs de condition de garde (fix + cofix)
barras
2006-05-12
*
une fonction pouvant calculer le gcd en coq
letouzey
2006-05-11
*
quelques ajouts venant des fichiers de Evelyne C.
letouzey
2006-05-11
*
decidabilite de InA
letouzey
2006-05-11
*
Comments about profiling
herbelin
2006-05-11
*
Oubli des symboles du Latin-1
herbelin
2006-05-11
*
Duplication du fichier FSetProperties pour les ensembles Weak.
letouzey
2006-05-11
*
r9089@thot: notin | 2006-05-10 14:40:51 +0200
notin
2006-05-11
*
correction bugs dans Cbv (beta n-aire)
barras
2006-05-10
*
Conformité nouveaux principes: Declare Module non utilisable pour définir u...
herbelin
2006-05-10
*
Centralisation de la détection lettre/symbole par le lexeur dans les plages ...
herbelin
2006-05-10
*
subst. explicites avec vecteurs
barras
2006-05-09
*
Correcting an old bug during generation of generale recursive functions.
jforest
2006-05-09
*
+ correcting a bug in general recursive function (match e with _ => match f e...
jforest
2006-05-07
*
doc du *in* de match/with
barras
2006-05-05
*
Protection mode Debug On contre Ctrl-D
herbelin
2006-05-05
*
Correction in generate_graph (now handles fun _ => fix ....)
jforest
2006-05-05
*
amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)
barras
2006-05-05
*
Vieux bug de fin 2004 gardé pour mémoire
herbelin
2006-05-05
*
Correction comportement clause _ du match goal
herbelin
2006-05-05
*
un Zgcd general gardant trace des coefs
letouzey
2006-05-05
*
encore un correctif sur le rewrite H in setoid:
letouzey
2006-05-05
*
- intégration de la modification suggérée par L. Mamane: coqmktop passe ma...
notin
2006-05-04
*
Fixing two minor bugs in recdef and graph of function generation.
jforest
2006-05-03
*
fixed bug #804: removed useless reduction in fix guard checking
barras
2006-05-03
[next]