aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2000-12-25Alias variable_pathherbelin
2000-12-25Effet réorganisation Classopsherbelin
2000-12-25Un nom long pour les variables de section qui font classe ou coercion; réorg...herbelin
2000-12-25Bug vieux Matchherbelin
2000-12-25Bug prédicatherbelin
2000-12-25Traducteur automatique de scripts vernacherbelin
2000-12-22*** empty log message ***mayero
2000-12-22Typoherbelin
2000-12-22MAJherbelin
2000-12-22cleanallherbelin
2000-12-22Insertion COQPATHPREFIX pour isntallation localeherbelin
2000-12-22Oublisherbelin
2000-12-22MAJ V7herbelin
2000-12-22Mauvais numéro de version de camlp4 requisherbelin
2000-12-22Pour créer les archives distribuéesherbelin
2000-12-22Novembre -> Décembreherbelin
2000-12-22Création...herbelin
2000-12-22MAJherbelin
2000-12-22Traduction en francais de 'CHANGES' dont le contenu était en françaisherbelin
2000-12-21Re-MAJherbelin
2000-12-21MAJherbelin
2000-12-21Bug d'affichage à cause des << ... >>herbelin
2000-12-21Qualification des inductifs dans Print indherbelin
2000-12-20MAJherbelin
2000-12-20MAJherbelin
2000-12-20Toujours Inductionherbelin
2000-12-20espacementsherbelin
2000-12-20Bug prédicat old Case/Matchherbelin
2000-12-20Suppression warning variable de filtrage en majusculeherbelin
2000-12-20Code mortherbelin
2000-12-20MAJherbelin
2000-12-20Test pour empêcher 2 sections de même nomsherbelin
2000-12-20Oublié de supprimer du code mortherbelin
2000-12-20Bug mauvais environnement dans le test d'eta-conversionherbelin
2000-12-20Rétablissement de l'ancien comportement de Simpl sauf dans le cas mutuel ind...herbelin
2000-12-20Toujours Inductionherbelin
2000-12-20ajout ident_or_constrarg pour NewInductionherbelin
2000-12-20Induction/NewInductionherbelin
2000-12-20Bug dans l'utilisation de l'option debugherbelin
2000-12-20Import module force l'ouverture du module même s'il était déjà ouvert afi...herbelin
2000-12-20Bug norm_evar_pf; remplacement par l'insertion d'un noeud local_constraints q...herbelin
2000-12-20Ajout set_lcherbelin
2000-12-20Scripts de correction d'uriherbelin
2000-12-20MAJherbelin
2000-12-20Non verbose par défautherbelin
2000-12-19Correction pour les variables abstraites dans les Tactic Definitionsdelahaye
2000-12-19DEMOS passe et MUTUAL-EXCLUSION aussi modulo Realizerdelahaye
2000-12-19correction de bugs sur commit précédentherbelin
2000-12-19Découpage des différentes fonctionnalités de build_mutual et definition_st...herbelin
2000-12-19Export fonction testant si un inductive est un recordherbelin