aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2006-05-26Support des modules dans Coqdocnotin
2006-05-26removing a warningjforest
2006-05-24Adaptation de Coqdoc au nouveau add_globnotin
2006-05-24Suite changement précédence by de assertherbelin
2006-05-23MAJherbelin
2006-05-23MAJ proprÃiété svn:ignore sur test-suiteherbelin
2006-05-23Mise à jour dev/doc/changes.txt et ajout d'un mot sur TACTIC EXTENDherbelin
2006-05-23Restructuration dossier dev et mise à jour de certaines documentationsherbelin
2006-05-23Retour version 8852 de constrintern.mlherbelin
2006-05-23Erreur commit constrintern.mlherbelin
2006-05-23Changement de précédence de l'argument du by de assert; conséquences...herbelin
2006-05-23Modification de add_glob (support des modules dans Coqdoc)notin
2006-05-23Error during last commit (coq didn't compile)jforest
2006-05-23Ajout substl_named_decl pour mode Mapleherbelin
2006-05-23Correcting a bug with ocaml <= 3.08.3 (Map.fold changing)jforest
2006-05-23Clarification role de library_part : renommage en remove_section_partherbelin
2006-05-23cleanning code jforest
2006-05-23PÃréouverture de la plupart des fichis pour éviter d'avoir à qualifierherbelin
2006-05-23Nouvelle implantation du polymorphisme de sorte pour les familles inductivesherbelin
2006-05-22un debut de propriétés concernant FMapletouzey
2006-05-22suite des marquages de types et opacifications de lemmes dans les wrappers Makeletouzey
2006-05-22Correcting a bug in identifiers manipulation jforest
2006-05-22LetTuple are now supported in Functionjforest
2006-05-22Modification de l'appel à coqdoc (COQBIN)notin
2006-05-22encore un exemple ne marchant pas, ni avec omega ni avec romegaletouzey
2006-05-22MAJ suite placement automatiquement de Rlist au niveau prédicatif le plus ba...herbelin
2006-05-22MAJ suite placement automatiquement de Rlist au niveau prédicatif le plus ba...herbelin
2006-05-20auto with zarith genere des sous-lemmes silencieusement, letouzey
2006-05-20"subst." works now even when it exists an hypothesis have the form "x=x" in t...jforest
2006-05-20suite tentative pour permettre l'utilisation de modules de FSetsletouzey
2006-05-19on cache autant que possible Raw dans FSet(Weak)List.Makeletouzey
2006-05-19tests de Romegaletouzey
2006-05-19Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsortherbelin
2006-05-18ajout de mes modifs recentesletouzey
2006-05-18git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8829 85f007b7-540e-04...letouzey
2006-05-18Dépendances pour List.vnotin
2006-05-17Correcting a bug in matching context on if. jforest
2006-05-17Typo dans List.vnotin
2006-05-17updating Function documentationjforest
2006-05-17Ajout de [count_occ] dans List.vnotin
2006-05-16etoffage des notions de permutations (a la fois List.Permutation et Permutati...letouzey
2006-05-16Typo dans CREDITSnotin
2006-05-15ajout de theories/FSets/DecidableTypeEx.vletouzey
2006-05-153*rienletouzey
2006-05-15ajout d'exemples de decidable typesletouzey
2006-05-15petit ajout concernant InAletouzey
2006-05-14On remet plutot l'ancien nom Zgcd_is_pos au lieu de Zgcd_posletouzey
2006-05-14In_dec de nouveau transparentletouzey
2006-05-14reparartion d'un petit oubli cassant PrecedenceGraphletouzey
2006-05-13typoletouzey