aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Update Program/subtac documentation.Gravatar msozeau2006-06-01
* Fix some nasty bug with the evars-to-dependent sum encoding.Gravatar msozeau2006-06-01
* bug in alpha-conversionGravatar jforest2006-06-01
* reparation bug #1128Gravatar letouzey2006-06-01
* Fusion if.v et If.v (MacOS X ne sait pas distinguer la casse)Gravatar herbelin2006-05-31
* Fusion destruct.v et Destruct.v (MacOS X ne sait pas distinguer la casseGravatar herbelin2006-05-31
* ajout de QArith dans les theories standardsGravatar letouzey2006-05-31
* petits ajoutsGravatar letouzey2006-05-31
* Replacing the old version of "functional induction" with the new one. Gravatar jforest2006-05-31
* Colorisation dans CoqideGravatar notin2006-05-31
* retour au comportement antérieur pour une application de foncteur: Gravatar letouzey2006-05-30
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* Correction bug #990 (LoadPath et option -R de coqideGravatar notin2006-05-30
* * 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