aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* Nouveau choix pour l'intros initialGravatar delahaye2000-11-24
* On n'introduit que des produits non dependantsGravatar delahaye2000-11-23
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* Reparation IsMutConstruct + TransparentGravatar mohring2000-11-23
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* PatternMatchingFailure n'etait pas rattrapeeGravatar herbelin2000-11-21
* Bugs make_tuple et existS_patternGravatar herbelin2000-11-21
* Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...Gravatar herbelin2000-11-20
* Utilisation de global_reference dans patternGravatar herbelin2000-11-20
* Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...Gravatar herbelin2000-11-20
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 00:14:19 +0000