aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* methode exportGravatar filliatr2000-11-15
* Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...Gravatar herbelin2000-11-10
* Bug et simplification nouvel InductionGravatar herbelin2000-11-09
* Nettoyage Names suiteGravatar herbelin2000-11-07
* Changement/extension dans les noms de parseurs de GrammarGravatar herbelin2000-11-07
* Marre de ces noms stupides IAvoid and co; changé en IntroAvoid and co; bah.....Gravatar herbelin2000-11-06
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* compilation des fichiers ml4 sans GNUseriesGravatar filliatr2000-11-03
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* - simplification Makefile (compilation des fichiers .ml'; pas encore parfaitGravatar filliatr2000-10-31
* .old virés (CVS est là pour ca)Gravatar filliatr2000-10-31
* Remplacement de Tauto et IntuitionGravatar delahaye2000-10-30
* erreur dans intro_gen corrigéeGravatar filliatr2000-10-27
* Intro choue si le nom d'hypothse existe au lieu de mettre un avertissementGravatar herbelin2000-10-27
* Ajoute : Ast dans la regle de grammaireGravatar mayero2000-10-27
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Changement parser par défaut dans SyntaxGravatar herbelin2000-10-18
* Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...Gravatar herbelin2000-10-13
* C'était pas le bon env dans build_termGravatar herbelin2000-10-11
* Prise en compte de Let à certains endroitsGravatar herbelin2000-10-11
* Prise en compte de l'env local dans make_apply_entryGravatar herbelin2000-10-11
* Prise en compte de Let dans build_dependent_inductiveGravatar herbelin2000-10-11
* Bug ordre dans push_relsGravatar herbelin2000-10-10
* Correction incompatibilites dans la fn des types des inductifsGravatar herbelin2000-10-06
* Mise en page de Print HintGravatar herbelin2000-10-06
* Bug de conflit de nommage d'hyp d'induction dans l'Induction fonctionnant dan...Gravatar herbelin2000-10-05
* Code mortGravatar herbelin2000-10-04
* code mortGravatar herbelin2000-10-04
* Rebranchement de la tactique LetGravatar herbelin2000-10-03
* L'argument de Refine est un terme ouvertGravatar herbelin2000-10-03
* mise en pageGravatar herbelin2000-10-03
* Renommage AppL en AppGravatar herbelin2000-10-01
* Plus de whd_castapp_stackGravatar herbelin2000-10-01
* Déplacement 'a reference et binder_kind de Term vers RawtermGravatar herbelin2000-10-01
* Code mortGravatar herbelin2000-10-01
* Elimination de coupures...Gravatar herbelin2000-10-01
* Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...Gravatar herbelin2000-09-26
* Abstraction de constrGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* nettoyageGravatar herbelin2000-09-10
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* cosmétiqueGravatar herbelin2000-08-28
* messages d'erreurGravatar herbelin2000-07-28
* Plus de piquants dans les actions des grammaires; nom de la grammaire pris co...Gravatar herbelin2000-07-28
* retablissement make doc et make minicoqGravatar filliatr2000-07-25
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 20:52:43 +0000