| Commit message (Expand) | Author | Age |
... | |
* | Test synchronisation chargement objets non logiques | herbelin | 2006-04-15 |
* | Si un fixpoint a plusieurs arguments, mais un seul de type inductif, | letouzey | 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-14 |
* | MAJ 8.1-APP | herbelin | 2006-04-13 |
* | MAJ 8.1-APP | herbelin | 2006-04-13 |
* | 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-12 |
* | 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-11 |
* | 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-10 |
* | Finalement, scopes utiles pour option 'where' (cf bug #1132) | herbelin | 2006-04-07 |
* | - Documentation of the Program tactics. | msozeau | 2006-04-07 |
* | 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-06 |
* | 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-05 |
* | Bug index addendum à cause mauvaise utilisation asection dans Helm.tex | herbelin | 2006-04-04 |
* | Correction bug 1119 (inversion marche a moitie dans Type) | herbelin | 2006-04-02 |
* | Petite actualisation FAQ | herbelin | 2006-03-31 |
* | Amendement impression evar pour affichage des Meta par 'info' | herbelin | 2006-03-31 |
* | Réajout de eq_rec_eq oublié lors de la modularisation de Eqdep | herbelin | 2006-03-30 |
* | 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-29 |
* | 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-28 |
* | 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-27 |
* | r8709@thot: notin | 2006-03-25 01:48:46 +0100 | notin | 2006-03-25 |