aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2001-01-30Bug fixed: the case [ id : ?1 -> ?2 |- ?] was missing in tauto_mainsacerdot
2001-01-30backtrack sur le lexeur de la V6filliatr
2001-01-29pas de warning avec Opaque quand is_silentfilliatr
2001-01-29As an heuristic, now both in tauto and intuition we try to avoid the initialsacerdot
2001-01-27make docherbelin
2001-01-27Ré-introduction des implicites à la volée dans la définition des inductifsherbelin
2001-01-27Simplification Impargsherbelin
2001-01-27Suppression du retrait du répertoire doc de l'archive tar-gzip-éeherbelin
2001-01-27Ajout alias mutual_inductive_path = section_pathherbelin
2001-01-27Factorisation du '.' finalherbelin
2001-01-27make docherbelin
2001-01-27Ré-introduction des implicites à la volée dans la définition des inductifsherbelin
2001-01-25Modif de l'axiomatisation pour enlever les /\ de _nemayero
2001-01-25Remplacement d'un bug non documente par un autre documente dans quantify_extr...herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 17:14:19 +0000