aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* Correction d'un bug lorsque des Variables sont clearees dans le but courantGravatar delahaye2000-11-23
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* Affichage des paths avec des '.', 2eme; prise en compte qualidGravatar herbelin2000-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
* NettoyageGravatar herbelin2000-11-22
* Tout est deja traite dans TacinterpGravatar delahaye2000-11-21
* Traitement du pretty-print des RedexpGravatar delahaye2000-11-21
* Prise en compte noms longsGravatar 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
* Modification de la table des tactic Definitions pour eviter l'ecritureGravatar mohring2000-11-07
* Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...Gravatar herbelin2000-11-06
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Tactiques utilisateur + debuggerGravatar delahaye2000-10-30
* Clarification message d'erreurGravatar herbelin2000-10-28
* Chasse au Cast de CastGravatar herbelin2000-10-27
* Essai de remplacement du whd_betaiotaevar de Qed par un whd_iseGravatar herbelin2000-10-26
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Code redondantGravatar herbelin2000-10-13
* Code redondantGravatar herbelin2000-10-13
* Renommage des find_m*typeGravatar herbelin2000-10-11
* Suppression d'un Cast inutileGravatar herbelin2000-10-05
* Utilisation de local_strong plutôt que strong buggé avec défs locales (2ème)Gravatar herbelin2000-10-04
* Utilisation de local_strong plutôt que strong buggé avec défs localesGravatar herbelin2000-10-04
* Ajout LetIn dans prim_extractorGravatar herbelin2000-10-04
* Elimination des coupures sur le type constantGravatar herbelin2000-10-04
* Ajout castedopenconstrargGravatar herbelin2000-10-03
* Rebranchement de la tactique LetGravatar herbelin2000-10-03
* Renommage AppL en AppGravatar herbelin2000-10-01
* Plus de whd_castappGravatar herbelin2000-10-01
* Plus de whd_castapp_stackGravatar 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
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Pattern matching de sous-termesGravatar delahaye2000-08-17
* 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
* Passage à des contextes de vars et de rels pouvant contenir des déclaration...Gravatar herbelin2000-07-24
* Pattern -> parsingGravatar delahaye2000-07-21
* Modifs d'interpretation de patternsGravatar delahaye2000-07-21
* portage RefineGravatar filliatr2000-07-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 20:20:05 +0000