aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Hint Unfold Local + commentairesGravatar mohring2000-12-12
* Reparation Intro sans nom qui ne reduisait pas le but quand celui-ciGravatar mohring2000-12-12
* message d'erreurGravatar herbelin2000-12-06
* Divers bugs LetTacGravatar herbelin2000-12-06
* caractere opaque des constantes repris en compteGravatar filliatr2000-12-04
* Portage d'AutoRewriteGravatar delahaye2000-12-02
* Nouveau long long avec Coq en têteGravatar herbelin2000-11-29
* Prise en compte du repertoire dans le section path; utilisation de dirpath po...Gravatar herbelin2000-11-28
* Elimination du 'Gravatar delahaye2000-11-28
* Prise en compte des let-in dans les fonctions de réduction pour les tactiquesGravatar herbelin2000-11-27
* Appel des constantes globaux par des noms absolusGravatar herbelin2000-11-26
* Distinction claire entre Induction (nom interne : raw_induct) et le nouvel in...Gravatar herbelin2000-11-26
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 23:24:01 +0000