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
*
Doc for Combined Scheme.
msozeau
2006-12-23
*
Addition of a "Combined Scheme" vernacular command for building the conjuncti...
msozeau
2006-12-23
*
Default tactic for solving goals.
msozeau
2006-12-22
*
remplacement d'un test d'egalite par un test de convertibilite dans injection...
jforest
2006-12-22
*
typo malencontreuse
filliatr
2006-12-21
*
Adaptation à Subversion 1.4
notin
2006-12-19
*
reparation bug 1239
letouzey
2006-12-17
*
Changement dans ring et field, beaucoup de correction d'erreurs,
bgregoir
2006-12-15
*
contrib/dp: tactique ergo (voir ergo.lri.fr)
filliatr
2006-12-15
*
Confusion sur le paramètre à donner à concrete_name lors du commit 9450
herbelin
2006-12-14
*
Reimplemented equality generation for pattern matching at typing time. First ...
msozeau
2006-12-14
*
Alignement de la politique de renommage de rename_bound_var (utilisé pour
herbelin
2006-12-13
*
test condition de garde
barras
2006-12-13
*
svn:ignore
herbelin
2006-12-13
*
Dépliage du terme d'induction avant suppression quand celui-ci est un
herbelin
2006-12-13
*
Correction du bug #1273, deuxième version (avec des shémas d'elimination pl...
notin
2006-12-12
*
Correction du bug #1273 (problème avec les paramètres non récursivement un...
notin
2006-12-12
*
Subtac: work on cases.
msozeau
2006-12-12
*
nouvelle indentation des scripts
barras
2006-12-12
*
cosmetique
barras
2006-12-12
*
Variable print_instances pour déboguer les instances d'evar
herbelin
2006-12-12
*
Dépendence inutile
herbelin
2006-12-12
*
AllÃègement de syntxe suite à l'introduction de l'unif pattern
herbelin
2006-12-12
*
Bug nommage Zgt_trans_succ
herbelin
2006-12-12
*
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
[next]