aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* - 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
* Typo dans List.vGravatar notin2006-05-17
* updating Function documentationGravatar jforest2006-05-17
* Ajout de [count_occ] dans List.vGravatar notin2006-05-17
* etoffage des notions de permutations (a la fois List.Permutation et Permutati...Gravatar letouzey2006-05-16
* Typo dans CREDITSGravatar notin2006-05-16
* ajout de theories/FSets/DecidableTypeEx.vGravatar letouzey2006-05-15
* 3*rienGravatar letouzey2006-05-15
* ajout d'exemples de decidable typesGravatar letouzey2006-05-15
* petit ajout concernant InAGravatar letouzey2006-05-15
* On remet plutot l'ancien nom Zgcd_is_pos au lieu de Zgcd_posGravatar letouzey2006-05-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 18:38:36 +0000