aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2000-11-23On n'introduit que des produits non dependantsdelahaye
2000-11-23print_id, print_sp -> pr_id, pr_spherbelin
2000-11-23Reparation IsMutConstruct + Transparentmohring
2000-11-22Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...herbelin
2000-11-21PatternMatchingFailure n'etait pas rattrapeeherbelin
2000-11-21Bugs make_tuple et existS_patternherbelin
2000-11-20Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...herbelin
2000-11-20Utilisation de global_reference dans patternherbelin
2000-11-20Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...herbelin
2000-11-15methode exportfilliatr
2000-11-10Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...herbelin
2000-11-09Bug et simplification nouvel Inductionherbelin
2000-11-07Nettoyage Names suiteherbelin
2000-11-07Changement/extension dans les noms de parseurs de Grammarherbelin
2000-11-06Marre de ces noms stupides IAvoid and co; changé en IntroAvoid and co; bah.....herbelin
2000-11-06nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...filliatr
2000-11-03compilation des fichiers ml4 sans GNUseriesfilliatr
2000-11-02correction Abstract (et make world passe!)filliatr
2000-11-02suppression des (* open Generic *)filliatr
2000-10-31- simplification Makefile (compilation des fichiers .ml'; pas encore parfaitfilliatr
2000-10-31.old virés (CVS est là pour ca)filliatr
2000-10-30Remplacement de Tauto et Intuitiondelahaye
2000-10-27erreur dans intro_gen corrigéefilliatr
2000-10-27Intro choue si le nom d'hypothse existe au lieu de mettre un avertissementherbelin
2000-10-27Ajoute : Ast dans la regle de grammairemayero
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
2000-10-18Renommage canonique :herbelin
2000-10-18Changement parser par défaut dans Syntaxherbelin
2000-10-13Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...herbelin
2000-10-11C'était pas le bon env dans build_termherbelin
2000-10-11Prise en compte de Let à certains endroitsherbelin
2000-10-11Prise en compte de l'env local dans make_apply_entryherbelin
2000-10-11Prise en compte de Let dans build_dependent_inductiveherbelin
2000-10-10Bug ordre dans push_relsherbelin
2000-10-06Correction incompatibilites dans la fn des types des inductifsherbelin
2000-10-06Mise en page de Print Hintherbelin
2000-10-05Bug de conflit de nommage d'hyp d'induction dans l'Induction fonctionnant dan...herbelin
2000-10-04Code mortherbelin
2000-10-04code mortherbelin
2000-10-03Rebranchement de la tactique Letherbelin
2000-10-03L'argument de Refine est un terme ouvertherbelin
2000-10-03mise en pageherbelin
2000-10-01Renommage AppL en Appherbelin
2000-10-01Plus de whd_castapp_stackherbelin
2000-10-01Déplacement 'a reference et binder_kind de Term vers Rawtermherbelin
2000-10-01Code mortherbelin
2000-10-01Elimination de coupures...herbelin
2000-09-26Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...herbelin
2000-09-14Abstraction de constrherbelin
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 23:37:36 +0000