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
*
Backtrack sur suppression des vars anonymes des contextes d'evars (echec Case...
herbelin
2006-12-12
*
MAJ
herbelin
2006-12-12
*
Test bug #932
herbelin
2006-12-12
*
Correction bug #1041 (double cause : non évitement des noms existants en
herbelin
2006-12-12
*
correction Open Local Scope (Ring)
bgregoir
2006-12-11
*
Changement dans le kernel :
bgregoir
2006-12-11
*
Évitement noms de constructeurs dans les motifs de filtrage de "match" (suite)
herbelin
2006-12-09
*
Évitement des noms de constructeurs dans les motifs de filtrage de "match"
herbelin
2006-12-09
*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9423 85f007b7-540e-04...
filliatr
2006-12-09
*
bug condition de garde
barras
2006-12-08
*
dp
filliatr
2006-12-08
*
contrib/dp
filliatr
2006-12-08
*
Pas d'escamotage des noms réservés si Set Printing All actibvé
herbelin
2006-12-08
*
Suite ajout option -output-context
herbelin
2006-12-08
*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9415 85f007b7-540e-04...
filliatr
2006-12-08
*
Ajout d'une option -output-context qui affiche le contexte en CCI pur à la
herbelin
2006-12-08
*
Correction typo règle réduction du fix chapitre CCI
herbelin
2006-12-08
*
Subtac bug fix, add list take example.
msozeau
2006-12-08
*
MAJ
herbelin
2006-12-03
*
Remplacement de la dépendance de G_vernac en G_constr (source
herbelin
2006-12-03
*
add a comment about Show Existentials and a question about case_eq
jnarboux
2006-12-01
*
Fork of cases impl for subtac.
msozeau
2006-11-29
*
correction du bug : VM value extraction error (PR#1290)
bgregoir
2006-11-29
*
The $(BEST) binaries symlinks depend on existence of target, not newness.
lmamane
2006-11-27
*
Functional graph merging deals with letins.
courtieu
2006-11-24
*
Fixed the graph merging parameter order.
courtieu
2006-11-24
*
Fixed the -emacs option which was always On.
courtieu
2006-11-24
*
Fixing syntax and parameter order in functional graph merging.
courtieu
2006-11-23
*
Code mort découvert par Matthieu
herbelin
2006-11-22
*
Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms de
herbelin
2006-11-21
*
un caractere blanc parasite dans svn:ignore
letouzey
2006-11-21
*
Changing merging functional scheme syntax.
courtieu
2006-11-20
*
Correction boucle du parseur en cas de caractÃère non unicode
herbelin
2006-11-20
*
Suppression du type 'tac dans les abstract_argument_type: devenu inutile
herbelin
2006-11-20
*
Dépendance inutile en Tacexpr, de proofs, qui se compile en principe après
herbelin
2006-11-19
*
mult_sym, plus_sym -> mult_comm, plus_comm
herbelin
2006-11-19
*
MAJ
herbelin
2006-11-19
*
Raffinement de l'unification de "apply": mémorisation de certains
herbelin
2006-11-19
*
Code mort (duplication de code dans reductionops.ml)
herbelin
2006-11-18
*
The emacs-U option now does not output *any* char above 250.
courtieu
2006-11-17
*
Small fix in functional graph merging.
courtieu
2006-11-16
*
suppression de code mort (avec bug de nom)
letouzey
2006-11-16
*
pb avec r9379 + modifs dans ring
barras
2006-11-16
*
Work on dep types pattern matching
msozeau
2006-11-16
*
suite de r9362: reconnaissance de qqs injections entre nat, N et Z
barras
2006-11-16
*
Adaptation à FreeBSD
notin
2006-11-16
*
Some usability enhancements.
msozeau
2006-11-15
*
Better solve using tactics impl.
msozeau
2006-11-13
*
Correction de la seconde partie du bug #1278
jforest
2006-11-13
*
Correction de la premiere partie du #1278 (but non referme en cas d'echec)
jforest
2006-11-13
[next]