aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Nouveau mécanisme pour les modules interactifs : les arguments deGravatar herbelin2006-04-16
* Added code to support "Program Lemma/Example... etc"Gravatar msozeau2006-04-16
* Inversion de l'ordre de chargement des objets logiques et non logiquesGravatar herbelin2006-04-15
* Tests notationsGravatar herbelin2006-04-15
* Test synchronisation chargement objets non logiquesGravatar herbelin2006-04-15
* Si un fixpoint a plusieurs arguments, mais un seul de type inductif, Gravatar letouzey2006-04-14
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 15:42:14 +0000