aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2000-07-20tests Refinefilliatr
2000-07-19Quelques (*i*) pour ne pas casser oczmlwebcoq
2000-07-05Adaptation pour Alpha.delahaye
2000-07-05Adaptation pour alpha.delahaye
2000-07-04correctionmayero
2000-07-03ajoutsmayero
2000-07-03Opaque pas encore implementee; syntax langage tactiquesfilliatr
2000-07-03Traduction de syntaxe vers ltacdelahaye
2000-07-03Correction de Cofixdelahaye
2000-07-01Plus de env et sigma dans get_arity, plus de sigma dans make_arityherbelin
2000-07-01Précalcul de la forme canonique des constructeurs et arités pour traiter le...herbelin
2000-07-01Ajout fonctions sur les aritésherbelin
2000-07-01Plus de env et sigma dans get_arity, plus de sigma dans make_arityherbelin
2000-07-01Précalcul de la forme canonique des constructeurs et arités pour traiter le...herbelin
2000-07-01Séparation des caractères spéciaux par un blancherbelin
2000-07-01Retrait des parenthèses inutiles autour des tactiquesherbelin
2000-07-01Extension de find_inductive aux co-inductifs et renommage en find_rectypeherbelin
2000-07-01Le bon type pour list_fold_right_and_leftherbelin
2000-07-01index devenu list_index échoue maintenant avec Not_found et plus Failureherbelin
2000-07-01Bug: on tentait de déclarer un schéma d'induction pour un coinductifherbelin
2000-07-01Extension de find_inductive aux co-inductifs et renommage en find_rectypeherbelin
2000-06-30fonction list_fold_left_right pas definiefilliatr
2000-06-29Capture erreur de create_processherbelin
2000-06-29Ajout list_fold_right_and_leftherbelin
2000-06-29MAJherbelin
2000-06-29Utilisation du STRIP de config/Makefile pour gérer le mode profileherbelin
2000-06-29Renommage mk_unsafe_judgment en get_judgment_of; ajout get_assumption_ofherbelin
2000-06-29Séparation des contraintes de type et de valeur dans pretypingherbelin
2000-06-29Relative prend sigma en plus pour la normalisation du message d'erreurherbelin
2000-06-29Broutillesherbelin
2000-06-29Ajout make_typed_lazyherbelin
2000-06-29Normalisation des Evar avant génération des erreursherbelin
2000-06-29Bricolesherbelin
2000-06-29Renommage mk_unsafe_judgment en get_judgment_ofherbelin
2000-06-29Extension de l'inférence des types des lambdas du prédicatherbelin
2000-06-29Achèvement abstraction du mécanisme (optionnel) de castherbelin
2000-06-29Rienherbelin
2000-06-29Essai de simplification compte tenu de l'info de locationherbelin
2000-06-28Modifs de presentation.delahaye
2000-06-28Rattrapage d'un Not_found pour les VAR's.delahaye
2000-06-27Retrait du 'strip' en cas de profilingherbelin
2000-06-21$BINDER -> BINDERfilliatr
2000-06-21 - $BINDER -> BINDER dans g_constr.ml4 (=> erreur syntax Fix)filliatr
2000-06-21Require Plus ajoutefilliatr
2000-06-21bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> .vo...filliatr
2000-06-21portage EAuto et Ringfilliatr
2000-06-21Ringfilliatr
2000-06-21theories/Realsfilliatr
2000-06-21theories/Relationsfilliatr
2000-06-21theories/Setsfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 05:41:04 +0000