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
*
Added {measure x f} as a valid recursion order.
msozeau
2006-06-22
*
Mutually structurally recursive defs and rec using measures added.
msozeau
2006-06-22
*
Harmonisation de l'interprétation des intropattern
herbelin
2006-06-21
*
Wellfounded recursion using subtac working again.
msozeau
2006-06-20
*
Progress in new wf def typing.
msozeau
2006-06-20
*
Rewrite of the recursive defs handling in progress.
msozeau
2006-06-20
*
bug serieux efficacite de ltac
barras
2006-06-19
*
Ajout de tactiques expérimentales basée sur functional induction.
courtieu
2006-06-16
*
Report des modifications faites lors de la 8.0pl3 (ter)
notin
2006-06-15
*
Report des modifications faites lors de la 8.0pl3 (bis)
notin
2006-06-15
*
Report des modifications faites lors de la 8.0pl3
notin
2006-06-15
*
Typo in case of reference to dev/doc/changes.txt
lmamane
2006-06-15
*
MAJ
herbelin
2006-06-15
*
MAJ
herbelin
2006-06-14
*
A list of incompatibilities
herbelin
2006-06-14
*
ajout d'un argument with_clean a Indfun.functional_induction permettant de ch...
jforest
2006-06-13
*
Changement du index.html généré dans refman
notin
2006-06-13
*
rearrangement du code: deplacement du code effectuant functional
courtieu
2006-06-13
*
Typo in replace doc.
jforest
2006-06-12
*
Updating documentation of replace and correcting a typo in error message of r...
jforest
2006-06-12
*
changed comments.
courtieu
2006-06-12
*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8948 85f007b7-540e-04...
jforest
2006-06-12
*
Bug is_number
herbelin
2006-06-10
*
MAJ fichier dev/doc/changes.txt
herbelin
2006-06-10
*
ajout de la doc sur l'option -enable-geoproof de CoqIDE
jnarboux
2006-06-10
*
Suppression du répertoire distrib: il fait désormais partie du projet coq-d...
notin
2006-06-09
*
Commit doc Claudio Sacerdoti
herbelin
2006-06-09
*
Nouvelle MAJ
herbelin
2006-06-09
*
Déplacement vers archive coq-dev-tools/distrib
herbelin
2006-06-09
*
Nouvelle MAJ
herbelin
2006-06-09
*
ajout de la doc de classical_right et left
jnarboux
2006-06-09
*
MAJ liste fichiers doc stdlib
herbelin
2006-06-09
*
Modification déf de exists! pour éviter une éta-expansion et pouvoir être...
herbelin
2006-06-09
*
Adaptation Tactics.out et Cases.out au comportement actuel à défaut d'évit...
herbelin
2006-06-09
*
Bug suite déplacement Int.v dans ZArith
herbelin
2006-06-09
*
Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableT...
herbelin
2006-06-09
*
Ajout d'une option -with-geoproof à la configuration et à l'exécution
notin
2006-06-09
*
oups: il faut penser a fermer la porte en partant (d'un fixpoint)
letouzey
2006-06-09
*
changements de dernieres minutes pour la 8.1 beta:
letouzey
2006-06-09
*
Plus de Declare Module sans vrai type explicite
herbelin
2006-06-08
*
MAJ Makefile depend
herbelin
2006-06-08
*
nouvelle MAJ
herbelin
2006-06-08
*
Changement du type d'argument 'TacticArgType X' en un type
herbelin
2006-06-08
*
MAJ coqc.byte et coqmktop.byte
herbelin
2006-06-08
*
Réinitialisation de token_number à chaque compilation d'un nouveau fichier ...
notin
2006-06-08
*
Warning ocaml 3.09 pour variable inutile
herbelin
2006-06-08
*
Factorisation utilisation environnement dans make_pr_tac
herbelin
2006-06-08
*
reparation bug 1006
letouzey
2006-06-08
*
Correction du bug #728(1086) (ordre de sauvegarde des tactiques dans coqide)
notin
2006-06-08
*
Détection bug rawwit suitecorrection trou de typage create_arg
herbelin
2006-06-08
[next]