aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2000-07-21Modifs d'interpretation de patternsdelahaye
2000-07-20portage Refinefilliatr
2000-07-01Plus de env et sigma dans get_arity, plus de sigma dans make_arityherbelin
2000-07-01Extension de find_inductive aux co-inductifs et renommage en find_rectypeherbelin
2000-06-29Rienherbelin
2000-06-28Modifs de presentation.delahaye
2000-06-21bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> .vo...filliatr
2000-06-21portage EAuto et Ringfilliatr
2000-06-15Code mortherbelin
2000-06-03Retrait des lam_and_pop and co (2ème - bug)herbelin
2000-06-03Retrait des lam_and_pop and coherbelin
2000-06-02Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
2000-05-31Nettoyage de Genericherbelin
2000-05-31Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursherbelin
2000-05-25Déplacement de save_thm and co de PFedit vers Commandherbelin
2000-05-23Bug stupide d'ordre d'évaluationherbelin
2000-05-22suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsherbelin
2000-05-22Changement nommage des hypothèsesherbelin
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
2000-05-22Retour comportement de la version précédenteherbelin
2000-05-18bugsherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 14:54:02 +0000