| Age | Commit message (Expand) | Author |
|---|
| 2006-04-14 | Pas fier | herbelin |
| 2006-04-14 | mise a jour credits | cpaulin |
| 2006-04-14 | Enleve les commentaires | cpaulin |
| 2006-04-14 | Test files for subtac. | msozeau |
| 2006-04-14 | Maj configure, README, etc... | notin |
| 2006-04-14 | Premier jet annonce 8.1 | herbelin |
| 2006-04-14 | MAJ 8.1 | herbelin |
| 2006-04-14 | replacing whd_betaiotaevar_preserving_vm_cast | jforest |
| 2006-04-13 | MAJ 8.1-APP | herbelin |
| 2006-04-13 | MAJ 8.1-APP | herbelin |
| 2006-04-12 | Changement de licence pour le Tutoriel de Coq | notin |
| 2006-04-12 | Simplifying the proof of principles | jforest |
| 2006-04-12 | induction on multiple arguments made better: | courtieu |
| 2006-04-11 | Modification of "Show Intros": it now shows letins too. | courtieu |
| 2006-04-11 | adding a new tactic [intro_avoiding idl] which acts as intro but prevents the | jforest |
| 2006-04-11 | ajout d'entrées dans TODO et CHANGES (à re-mettre à jour avant la release) | courtieu |
| 2006-04-11 | patch pour contourner l'échec de type_of_applied_inductive sur un inductif a... | herbelin |
| 2006-04-10 | Fixes for new unification, not used in default version as it really changes u... | msozeau |
| 2006-04-10 | + Changing a little functional schemes types | jforest |
| 2006-04-10 | Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous... | msozeau |
| 2006-04-10 | New unification can solve the problem without eta-expansion, | msozeau |
| 2006-04-07 | Finalement, scopes utiles pour option 'where' (cf bug #1132) | herbelin |
| 2006-04-07 | - Documentation of the Program tactics. | msozeau |
| 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 |
