aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2006-06-21Harmonisation de l'interprétation des intropatternherbelin
2006-06-20Wellfounded recursion using subtac working again.msozeau
2006-06-20Progress in new wf def typing.msozeau
2006-06-20Rewrite of the recursive defs handling in progress.msozeau
2006-06-19bug serieux efficacite de ltacbarras
2006-06-16Ajout de tactiques expérimentales basée sur functional induction.courtieu
2006-06-15Report des modifications faites lors de la 8.0pl3 (ter)notin
2006-06-15Report des modifications faites lors de la 8.0pl3 (bis)notin
2006-06-15Report des modifications faites lors de la 8.0pl3notin
2006-06-15Typo in case of reference to dev/doc/changes.txtlmamane
2006-06-15MAJherbelin
2006-06-14MAJherbelin
2006-06-14A list of incompatibilitiesherbelin
2006-06-13ajout d'un argument with_clean a Indfun.functional_induction permettant de ch...jforest
2006-06-13Changement du index.html généré dans refmannotin
2006-06-13rearrangement du code: deplacement du code effectuant functionalcourtieu
2006-06-12Typo in replace doc. jforest
2006-06-12Updating documentation of replace and correcting a typo in error message of r...jforest
2006-06-12changed comments.courtieu
2006-06-12git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8948 85f007b7-540e-04...jforest
2006-06-10Bug is_numberherbelin
2006-06-10MAJ fichier dev/doc/changes.txtherbelin
2006-06-10ajout de la doc sur l'option -enable-geoproof de CoqIDEjnarboux
2006-06-09Suppression du répertoire distrib: il fait désormais partie du projet coq-d...notin
2006-06-09Commit doc Claudio Sacerdotiherbelin
2006-06-09Nouvelle MAJherbelin
2006-06-09Déplacement vers archive coq-dev-tools/distribherbelin
2006-06-09Nouvelle MAJherbelin
2006-06-09ajout de la doc de classical_right et leftjnarboux
2006-06-09MAJ liste fichiers doc stdlibherbelin
2006-06-09Modification déf de exists! pour éviter une éta-expansion et pouvoir être...herbelin
2006-06-09Adaptation Tactics.out et Cases.out au comportement actuel à défaut d'évit...herbelin
2006-06-09Bug suite déplacement Int.v dans ZArithherbelin
2006-06-09Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableT...herbelin
2006-06-09Ajout d'une option -with-geoproof à la configuration et à l'exécutionnotin
2006-06-09oups: il faut penser a fermer la porte en partant (d'un fixpoint)letouzey
2006-06-09changements de dernieres minutes pour la 8.1 beta: letouzey
2006-06-08Plus de Declare Module sans vrai type expliciteherbelin
2006-06-08MAJ Makefile dependherbelin
2006-06-08nouvelle MAJherbelin
2006-06-08Changement du type d'argument 'TacticArgType X' en un typeherbelin
2006-06-08MAJ coqc.byte et coqmktop.byteherbelin
2006-06-08Réinitialisation de token_number à chaque compilation d'un nouveau fichier ...notin
2006-06-08Warning ocaml 3.09 pour variable inutileherbelin
2006-06-08Factorisation utilisation environnement dans make_pr_tacherbelin
2006-06-08reparation bug 1006letouzey
2006-06-08Correction du bug #728(1086) (ordre de sauvegarde des tactiques dans coqide)notin
2006-06-08Détection bug rawwit suitecorrection trou de typage create_argherbelin
2006-06-07replace byherbelin
2006-06-07Correction trou de subject-reduction de create_arg dans genarg.mliherbelin