aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* Le bon choix, c'est finalement identifier = stringGravatar herbelin2000-12-15
* Mise en pageGravatar herbelin2000-12-15
* Mise en place d'un module Ident avec test de l'efficacité quand identifier=s...Gravatar herbelin2000-12-15
* Bug env vis à vis du let inGravatar herbelin2000-12-15
* pb niveauGravatar mayero2000-12-15
* suppression warning et calcule type dans replace_by_meta dans tous les casGravatar filliatr2000-12-15
* mise a jourGravatar filliatr2000-12-15
* - suppression mind_extract_paramsGravatar filliatr2000-12-15
* MAJGravatar herbelin2000-12-15
* Réparation de bugs de LoadPathGravatar herbelin2000-12-15
* Re-ajout des syntaxes Add LoadPath, Remove LoadPath, etc; ajout entrées 'Set...Gravatar herbelin2000-12-15
* Petite réorganisationGravatar herbelin2000-12-15
* Bug des locaux au premier niveau des modules qui disparaissaient de l'environ...Gravatar herbelin2000-12-15
* Bugs calcul du prédicat des Cases et CaseGravatar herbelin2000-12-15