| Age | Commit message (Expand) | Author |
|---|
| 2006-04-06 | versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmes | letouzey |
| 2006-04-06 | versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmes | letouzey |
| 2006-04-06 | ouverture du bon scope (positive_scope) derriere le constructeur Npos de N | letouzey |
| 2006-04-06 | Enlevement de message d'erreur garbage. | courtieu |
| 2006-04-05 | resolution du bug/souhait #1101 : rewrite setoid dans les hypotheses | letouzey |
| 2006-04-05 | MAJ Licence FAQ | herbelin |
| 2006-04-05 | on utilise explicitement Prop/iff pour certains morphismes pour eviter des wa... | letouzey |
| 2006-04-05 | Suppression du test Proof with <tac> | notin |
| 2006-04-05 | ajout d'un rattrapage d'erreur pour "induction using". | courtieu |
| 2006-04-04 | Bug index addendum à cause mauvaise utilisation asection dans Helm.tex | herbelin |
| 2006-04-02 | Correction bug 1119 (inversion marche a moitie dans Type) | herbelin |
| 2006-03-31 | Petite actualisation FAQ | herbelin |
| 2006-03-31 | Amendement impression evar pour affichage des Meta par 'info' | herbelin |
| 2006-03-30 | Réajout de eq_rec_eq oublié lors de la modularisation de Eqdep | herbelin |
| 2006-03-29 | Inductifs avec polymorphisme de sorte (version initiale) | herbelin |
| 2006-03-29 | Ajout array_fold_map', list_fold_map' et list_remove_first | herbelin |
| 2006-03-29 | pour coqdoc | letouzey |
| 2006-03-28 | Nommage explicite de certains "intro" pour préserver la compatibilité | herbelin |
| 2006-03-28 | - correction d'un bug dans coqdoc (multi_index) | notin |
| 2006-03-28 | Correction bug/typo dans splay_prod_assum et ajout decomp_sort | herbelin |
| 2006-03-28 | reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / Ordere... | letouzey |
| 2006-03-27 | Correction d'un bug dans Coqdoc (indentation & mots clés) | notin |
| 2006-03-27 | - correction du bug #1055 | notin |
| 2006-03-27 | appel Zenon sans prelude | filliatr |
| 2006-03-25 | r8709@thot: notin | 2006-03-25 01:48:46 +0100 | notin |
| 2006-03-25 | r8708@thot: notin | 2006-03-24 18:55:01 +0100 | notin |
| 2006-03-25 | r8686@thot: notin | 2006-03-20 19:29:09 +0100 | notin |
| 2006-03-24 | utilisation de la VM pour la normalisation finale de romega | letouzey |
| 2006-03-24 | Patch envoy\'e par Benjamin Gregoire, permettant de corriger | letouzey |
| 2006-03-23 | on ignore TAGS au niveau svn | letouzey |
| 2006-03-23 | correctifs de bug pour romega: | letouzey |
| 2006-03-23 | Correction d'un bug sur 'make doc' et modification des propriétés dans doc/ | notin |
| 2006-03-22 | Subtac fixes, single fixpoint definitions are working again. Added a toggle o... | msozeau |
| 2006-03-22 | Made pretyping a functor over a coercion implementation. Pretyping.Default us... | msozeau |
| 2006-03-22 | - Correction bug calcul mind_consnrealargs, introduit à la révision | herbelin |
| 2006-03-22 | - Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de | herbelin |
| 2006-03-21 | + destruct now works as induction on multiple arguments : | jforest |
| 2006-03-21 | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8650 85f007b7-540e-04... | letouzey |
| 2006-03-20 | Adding "New Functional Scheme" | jforest |
| 2006-03-18 | Documentation | herbelin |
| 2006-03-18 | MAJ documentation en syntaxe v8 | herbelin |
| 2006-03-18 | Bug BYTEFLAGS pour compilation bin/parser | herbelin |
| 2006-03-18 | Documentation mutual_inductive_body | herbelin |
| 2006-03-18 | Bug calcul consnrealargs + bug calcul occurrences non positives + modifs cosm... | herbelin |
| 2006-03-17 | MAJ debugging (et arrêt support version française) | herbelin |
| 2006-03-17 | Modification des propriétés (svn:executable) | notin |
| 2006-03-17 | ajout d'un debut de proprietes pour les FSetWeak | letouzey |
| 2006-03-16 | deux tags $ mal formes | letouzey |
| 2006-03-16 | propriete svn:keywords positionnee a Author Date Id Revision sur l'ensemble d... | letouzey |
| 2006-03-16 | afin que svn ignore les liens symb coqide et coqtop | letouzey |
