aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* * suite de la revision des wrappers MakeGravatar letouzey2006-05-30
* The "clean integration of subtac" patch.Gravatar msozeau2006-05-29
* Fix broken paths.Gravatar msozeau2006-05-29
* small changes Gravatar jforest2006-05-29
* Ajout d'alias pour prodT_rect et cie qui avaient été oublkÃiésGravatar herbelin2006-05-29
* - Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesGravatar herbelin2006-05-28
* Adaptation au passage de sig2 dans TypeGravatar herbelin2006-05-28
* Adaptation au passage de vector dans TypeGravatar herbelin2006-05-28
* Adaptation au passage de option dans TypeGravatar herbelin2006-05-28
* Ajout array_fold_map2Ã'Gravatar herbelin2006-05-28
* - Déplacement des types paramétriques prod, sum, option, identity,Gravatar herbelin2006-05-28
* Modification de la compilation de coqc et coqmktop pour éviter le problème ...Gravatar notin2006-05-26
* Added contrib/funind to the path for ocamldebug-coqGravatar courtieu2006-05-26
* Support des modules dans CoqdocGravatar notin2006-05-26
* removing a warningGravatar jforest2006-05-26
* Adaptation de Coqdoc au nouveau add_globGravatar notin2006-05-24
* Suite changement précédence by de assertGravatar herbelin2006-05-24
* MAJGravatar herbelin2006-05-23
* MAJ proprÃiété svn:ignore sur test-suiteGravatar herbelin2006-05-23
* Mise à jour dev/doc/changes.txt et ajout d'un mot sur TACTIC EXTENDGravatar herbelin2006-05-23
* Restructuration dossier dev et mise à jour de certaines documentationsGravatar herbelin2006-05-23
* Retour version 8852 de constrintern.mlGravatar herbelin2006-05-23
* Erreur commit constrintern.mlGravatar herbelin2006-05-23
* Changement de précédence de l'argument du by de assert; conséquences...Gravatar herbelin2006-05-23
* Modification de add_glob (support des modules dans Coqdoc)Gravatar notin2006-05-23
* Error during last commit (coq didn't compile)Gravatar jforest2006-05-23
* Ajout substl_named_decl pour mode MapleGravatar herbelin2006-05-23
* Correcting a bug with ocaml <= 3.08.3 (Map.fold changing)Gravatar jforest2006-05-23
* Clarification role de library_part : renommage en remove_section_partGravatar herbelin2006-05-23
* cleanning code Gravatar jforest2006-05-23
* PÃréouverture de la plupart des fichis pour éviter d'avoir à qualifierGravatar herbelin2006-05-23
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* un debut de propriétés concernant FMapGravatar letouzey2006-05-22
* suite des marquages de types et opacifications de lemmes dans les wrappers MakeGravatar letouzey2006-05-22
* Correcting a bug in identifiers manipulation Gravatar jforest2006-05-22
* LetTuple are now supported in FunctionGravatar jforest2006-05-22
* Modification de l'appel à coqdoc (COQBIN)Gravatar notin2006-05-22
* encore un exemple ne marchant pas, ni avec omega ni avec romegaGravatar letouzey2006-05-22
* MAJ suite placement automatiquement de Rlist au niveau prédicatif le plus ba...Gravatar herbelin2006-05-22
* MAJ suite placement automatiquement de Rlist au niveau prédicatif le plus ba...Gravatar herbelin2006-05-22
* auto with zarith genere des sous-lemmes silencieusement, Gravatar letouzey2006-05-20
* "subst." works now even when it exists an hypothesis have the form "x=x" in t...Gravatar jforest2006-05-20
* suite tentative pour permettre l'utilisation de modules de FSetsGravatar letouzey2006-05-20
* on cache autant que possible Raw dans FSet(Weak)List.MakeGravatar letouzey2006-05-19
* tests de RomegaGravatar letouzey2006-05-19
* Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsortGravatar herbelin2006-05-19
* ajout de mes modifs recentesGravatar letouzey2006-05-18
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8829 85f007b7-540e-04...Gravatar letouzey2006-05-18
* Dépendances pour List.vGravatar notin2006-05-18
* Correcting a bug in matching context on if. Gravatar jforest2006-05-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-23 11:05:38 +0000