aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Bug d'affichage à cause des << ... >>Gravatar herbelin2000-12-21
* Qualification des inductifs dans Print indGravatar herbelin2000-12-21
* MAJGravatar herbelin2000-12-20
* MAJGravatar herbelin2000-12-20
* Toujours InductionGravatar herbelin2000-12-20
* espacementsGravatar herbelin2000-12-20
* Bug prédicat old Case/MatchGravatar herbelin2000-12-20
* Suppression warning variable de filtrage en majusculeGravatar herbelin2000-12-20
* Code mortGravatar herbelin2000-12-20
* MAJGravatar herbelin2000-12-20
* Test pour empêcher 2 sections de même nomsGravatar herbelin2000-12-20
* Oublié de supprimer du code mortGravatar herbelin2000-12-20
* Bug mauvais environnement dans le test d'eta-conversionGravatar herbelin2000-12-20
* Rétablissement de l'ancien comportement de Simpl sauf dans le cas mutuel ind...Gravatar herbelin2000-12-20
* Toujours InductionGravatar herbelin2000-12-20
* ajout ident_or_constrarg pour NewInductionGravatar herbelin2000-12-20
* Induction/NewInductionGravatar herbelin2000-12-20
* Bug dans l'utilisation de l'option debugGravatar herbelin2000-12-20
* Import module force l'ouverture du module même s'il était déjà ouvert afi...Gravatar herbelin2000-12-20
* Bug norm_evar_pf; remplacement par l'insertion d'un noeud local_constraints q...Gravatar herbelin2000-12-20
* Ajout set_lcGravatar herbelin2000-12-20
* Scripts de correction d'uriGravatar herbelin2000-12-20
* MAJGravatar herbelin2000-12-20
* Non verbose par défautGravatar herbelin2000-12-20
* Correction pour les variables abstraites dans les Tactic DefinitionsGravatar delahaye2000-12-19
* DEMOS passe et MUTUAL-EXCLUSION aussi modulo RealizerGravatar delahaye2000-12-19
* correction de bugs sur commit précédentGravatar herbelin2000-12-19
* Découpage des différentes fonctionnalités de build_mutual et definition_st...Gravatar herbelin2000-12-19
* Export fonction testant si un inductive est un recordGravatar herbelin2000-12-19
* Amélioration affichage Print ALlGravatar herbelin2000-12-19
* PédagogieGravatar herbelin2000-12-19
* Correction associativite de Repeat/OrelseGravatar delahaye2000-12-19
* AutoRewrite n'ecrit plus de valeurs fonctionnelles sur disqueGravatar delahaye2000-12-19
* Bugs connus et non résolusGravatar herbelin2000-12-18
* MAJGravatar herbelin2000-12-18
* Renommages autour de NewInductionGravatar herbelin2000-12-18
* Code mortGravatar herbelin2000-12-18
* DocumentationGravatar herbelin2000-12-18
* Suppression de l'affichage des instances des ?nGravatar herbelin2000-12-18
* MAJGravatar herbelin2000-12-18
* Amélioration message d'erreur mauvais prédicatGravatar herbelin2000-12-18
* Export de it_mkProd_or_LetIn_name et it_mkLambda_or_LetIn_nameGravatar herbelin2000-12-18
* Debut de nettoyage de SimplGravatar mohring2000-12-18
* Mise a jourGravatar mohring2000-12-18
* Mise a jourGravatar mohring2000-12-18
* MAJGravatar herbelin2000-12-16
* Redondant or incompatible instantiations in clenv_assign now correctly trappedGravatar herbelin2000-12-16
* *** empty log message ***Gravatar herbelin2000-12-16
* Suppression du warning several default clausesGravatar herbelin2000-12-16
* Prise en compte modules/sections qualifiés dans SearchPattern et SearchRewriteGravatar herbelin2000-12-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 20:45:00 +0000