aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2001-01-24Ajout flush, diversherbelin
2001-01-24MAJherbelin
2001-01-24Protection contre l'échec de Unix.statherbelin
2001-01-24Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...herbelin
2001-01-24Prise en compte des noms longs dans les Hints et les Coercionsherbelin
2001-01-24Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...herbelin
2001-01-24MAJherbelin
2001-01-24Ajout global_vars_declherbelin
2001-01-24Réorganisation suite ajout de constantes locales dans les Recordsherbelin
2001-01-24Docherbelin
2001-01-24Ajout de constantes locales dans les Recordsherbelin
2001-01-22Retour en arrière sur le pb f_equal en attente meilleure solutionherbelin
2001-01-21Tests pourherbelin
2001-01-21Bug « f_equal » : arguments inférables par une unification des types qui n...herbelin
2001-01-19Nouveaux bugs instanciation d'evar par des evarherbelin
2001-01-19Prise en compte de constructeurs qualifiés dans les patternsherbelin
2001-01-19Nouveau module pour centraliser les chemins des constantes globales utilisée...herbelin
2001-01-19Ajout d'un parseur d'entiers sous forme de patternherbelin
2001-01-19Autour des quotations avec Casesherbelin
2001-01-19Réparation bug extensibilité de Constr.patternherbelin
2001-01-19Bugs encoreherbelin
2001-01-18Bug Identity Coercionherbelin
2001-01-17MAJherbelin
2001-01-15Essai d'axiomatisation des numeralmohring
2001-01-15Ajout de commentaire coqwebmohring
2001-01-15Raffinementsherbelin
2001-01-14Petit bug encoreherbelin
2001-01-14Bien sûr: bugs sur précédent commit; améliorationsherbelin
2001-01-14Prise en compte de l'allocation mémoire et affichage des résultats net du s...herbelin
2001-01-12Now Ring does not perform any more the same reduction twice.sacerdot
2001-01-12Comment fixedsacerdot
2001-01-11corr bug -mayero
2001-01-11Now reduction to normal form is done only when the term is notsacerdot
2001-01-11Many unuseful rewritings are no more done by Ring.sacerdot
2001-01-11Bug environnementherbelin
2001-01-11Mise a jour Rbasemohring
2001-01-09Meta Definition + Tactic Definitiondelahaye
2001-01-09Meta Definition -> Tactic Definitiondelahaye
2001-01-09Meta Definition -> Tactic Definitiondelahaye
2001-01-09Tactic Definition -> Meta Definitiondelahaye
2001-01-05Arite cachee de Match Context + Meta Definitiondelahaye
2001-01-04Rajout de la restriction de l'instance en cas d'unification de 2 variables ex...herbelin
2001-01-03Prise en compte des ??herbelin
2001-01-03Let doit etre utilise dans le mode de preuvedelahaye
2001-01-03Rattrapage d'erreur pour le Case + Eval Compute in pour Definitiondelahaye
2000-12-29Ajout du Let pour le langage de tactiquesdelahaye
2000-12-27Améliorationsherbelin
2000-12-27Bug installation non localeherbelin
2000-12-26MAJherbelin
2000-12-26Dernière MAJherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-26 07:54:34 +0000