aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Pas fierGravatar herbelin2006-04-14
* mise a jour creditsGravatar cpaulin2006-04-14
* Enleve les commentairesGravatar cpaulin2006-04-14
* Test files for subtac.Gravatar msozeau2006-04-14
* Maj configure, README, etc...Gravatar notin2006-04-14
* Premier jet annonce 8.1Gravatar herbelin2006-04-14
* MAJ 8.1Gravatar herbelin2006-04-14
* replacing whd_betaiotaevar_preserving_vm_cast Gravatar jforest2006-04-14
* MAJ 8.1-APPGravatar herbelin2006-04-13
* MAJ 8.1-APPGravatar herbelin2006-04-13
* Changement de licence pour le Tutoriel de CoqGravatar notin2006-04-12
* Simplifying the proof of principlesGravatar jforest2006-04-12
* induction on multiple arguments made better:Gravatar courtieu2006-04-12
* Modification of "Show Intros": it now shows letins too.Gravatar courtieu2006-04-11
* adding a new tactic [intro_avoiding idl] which acts as intro but prevents theGravatar jforest2006-04-11
* ajout d'entrées dans TODO et CHANGES (à re-mettre à jour avant la release)Gravatar courtieu2006-04-11
* patch pour contourner l'échec de type_of_applied_inductive sur un inductif a...Gravatar herbelin2006-04-11
* Fixes for new unification, not used in default version as it really changes u...Gravatar msozeau2006-04-10
* + Changing a little functional schemes types Gravatar jforest2006-04-10
* Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...Gravatar msozeau2006-04-10
* New unification can solve the problem without eta-expansion, Gravatar msozeau2006-04-10
* Finalement, scopes utiles pour option 'where' (cf bug #1132)Gravatar herbelin2006-04-07
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
* versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmesGravatar letouzey2006-04-06
* versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmesGravatar letouzey2006-04-06
* ouverture du bon scope (positive_scope) derriere le constructeur Npos de NGravatar letouzey2006-04-06
* Enlevement de message d'erreur garbage.Gravatar courtieu2006-04-06
* resolution du bug/souhait #1101 : rewrite setoid dans les hypotheses Gravatar letouzey2006-04-05
* MAJ Licence FAQGravatar herbelin2006-04-05
* on utilise explicitement Prop/iff pour certains morphismes pour eviter des wa...Gravatar letouzey2006-04-05
* Suppression du test Proof with <tac>Gravatar notin2006-04-05
* ajout d'un rattrapage d'erreur pour "induction using".Gravatar courtieu2006-04-05
* Bug index addendum à cause mauvaise utilisation asection dans Helm.texGravatar herbelin2006-04-04
* Correction bug 1119 (inversion marche a moitie dans Type)Gravatar herbelin2006-04-02
* Petite actualisation FAQGravatar herbelin2006-03-31
* Amendement impression evar pour affichage des Meta par 'info'Gravatar herbelin2006-03-31
* Réajout de eq_rec_eq oublié lors de la modularisation de EqdepGravatar herbelin2006-03-30
* Inductifs avec polymorphisme de sorte (version initiale)Gravatar herbelin2006-03-29
* Ajout array_fold_map', list_fold_map' et list_remove_firstGravatar herbelin2006-03-29
* pour coqdocGravatar letouzey2006-03-29
* Nommage explicite de certains "intro" pour préserver la compatibilitéGravatar herbelin2006-03-28
* - correction d'un bug dans coqdoc (multi_index)Gravatar notin2006-03-28
* Correction bug/typo dans splay_prod_assum et ajout decomp_sortGravatar herbelin2006-03-28
* reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / Ordere...Gravatar letouzey2006-03-28
* Correction d'un bug dans Coqdoc (indentation & mots clés)Gravatar notin2006-03-27
* - correction du bug #1055Gravatar notin2006-03-27
* appel Zenon sans preludeGravatar filliatr2006-03-27
* r8709@thot: notin | 2006-03-25 01:48:46 +0100Gravatar notin2006-03-25
* r8708@thot: notin | 2006-03-24 18:55:01 +0100Gravatar notin2006-03-25
* r8686@thot: notin | 2006-03-20 19:29:09 +0100Gravatar notin2006-03-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-04 11:54:40 +0000