aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* ajout d'un argument with_clean a Indfun.functional_induction permettant de ch...Gravatar jforest2006-06-13
* Changement du index.html généré dans refmanGravatar notin2006-06-13
* rearrangement du code: deplacement du code effectuant functionalGravatar courtieu2006-06-13
* Typo in replace doc. Gravatar jforest2006-06-12
* Updating documentation of replace and correcting a typo in error message of r...Gravatar jforest2006-06-12
* changed comments.Gravatar courtieu2006-06-12
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8948 85f007b7-540e-04...Gravatar jforest2006-06-12
* Bug is_numberGravatar herbelin2006-06-10
* MAJ fichier dev/doc/changes.txtGravatar herbelin2006-06-10
* ajout de la doc sur l'option -enable-geoproof de CoqIDEGravatar jnarboux2006-06-10
* Suppression du répertoire distrib: il fait désormais partie du projet coq-d...Gravatar notin2006-06-09
* Commit doc Claudio SacerdotiGravatar herbelin2006-06-09
* Nouvelle MAJGravatar herbelin2006-06-09
* Déplacement vers archive coq-dev-tools/distribGravatar herbelin2006-06-09
* Nouvelle MAJGravatar herbelin2006-06-09
* ajout de la doc de classical_right et leftGravatar jnarboux2006-06-09
* MAJ liste fichiers doc stdlibGravatar herbelin2006-06-09
* Modification déf de exists! pour éviter une éta-expansion et pouvoir être...Gravatar herbelin2006-06-09
* Adaptation Tactics.out et Cases.out au comportement actuel à défaut d'évit...Gravatar herbelin2006-06-09
* Bug suite déplacement Int.v dans ZArithGravatar herbelin2006-06-09
* Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableT...Gravatar herbelin2006-06-09
* Ajout d'une option -with-geoproof à la configuration et à l'exécutionGravatar notin2006-06-09
* oups: il faut penser a fermer la porte en partant (d'un fixpoint)Gravatar letouzey2006-06-09
* changements de dernieres minutes pour la 8.1 beta: Gravatar letouzey2006-06-09
* Plus de Declare Module sans vrai type expliciteGravatar herbelin2006-06-08
* MAJ Makefile dependGravatar herbelin2006-06-08
* nouvelle MAJGravatar herbelin2006-06-08
* Changement du type d'argument 'TacticArgType X' en un typeGravatar herbelin2006-06-08
* MAJ coqc.byte et coqmktop.byteGravatar herbelin2006-06-08
* Réinitialisation de token_number à chaque compilation d'un nouveau fichier ...Gravatar notin2006-06-08
* Warning ocaml 3.09 pour variable inutileGravatar herbelin2006-06-08
* Factorisation utilisation environnement dans make_pr_tacGravatar herbelin2006-06-08
* reparation bug 1006Gravatar letouzey2006-06-08
* Correction du bug #728(1086) (ordre de sauvegarde des tactiques dans coqide)Gravatar notin2006-06-08
* Détection bug rawwit suitecorrection trou de typage create_argGravatar herbelin2006-06-08
* replace byGravatar herbelin2006-06-07
* Correction trou de subject-reduction de create_arg dans genarg.mliGravatar herbelin2006-06-07
* Ajout WhelpGravatar herbelin2006-06-07
* petites corrections dans la doc de functional xxx. Gravatar courtieu2006-06-07
* Nouveaux Parametres InductifsGravatar cpaulin2006-06-07
* Réparation coqtop.mlGravatar notin2006-06-07
* Changement de l'option -where: on vérifie si la variable d'environnement COQ...Gravatar notin2006-06-07
* functional induction can now be used with Gravatar jforest2006-06-07
* mise en texttt d'une commande.Gravatar courtieu2006-06-07
* Changements sur Functional xxx. Plus précis et plus exact.Gravatar courtieu2006-06-07
* Ajout de précisions dans la doc de functional scheme et consort +Gravatar courtieu2006-06-06
* this time it's good Gravatar jforest2006-06-06
* Error in last commit Gravatar jforest2006-06-06
* Debut modif parametres inductifs CICGravatar cpaulin2006-06-06
* protecting an uncaught exception Not_found Gravatar jforest2006-06-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 05:37:14 +0000