aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2000-09-10nettoyageherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Suppression de Abstherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-08-28cosmétiqueherbelin
2000-07-28messages d'erreurherbelin
2000-07-28Plus de piquants dans les actions des grammaires; nom de la grammaire pris co...herbelin
2000-07-25retablissement make doc et make minicoqfilliatr
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-19 04:09:55 +0000