aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2000-11-10Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...herbelin
2000-11-07Modification de la table des tactic Definitions pour eviter l'ecrituremohring
2000-11-06Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...herbelin
2000-11-06nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...filliatr
2000-11-02correction Abstract (et make world passe!)filliatr
2000-11-02suppression des (* open Generic *)filliatr
2000-10-30Tactiques utilisateur + debuggerdelahaye
2000-10-28Clarification message d'erreurherbelin
2000-10-27Chasse au Cast de Castherbelin
2000-10-26Essai de remplacement du whd_betaiotaevar de Qed par un whd_iseherbelin
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
2000-10-18Renommage canonique :herbelin
2000-10-13Code redondantherbelin
2000-10-13Code redondantherbelin
2000-10-11Renommage des find_m*typeherbelin
2000-10-05Suppression d'un Cast inutileherbelin
2000-10-04Utilisation de local_strong plutôt que strong buggé avec défs locales (2ème)herbelin
2000-10-04Utilisation de local_strong plutôt que strong buggé avec défs localesherbelin
2000-10-04Ajout LetIn dans prim_extractorherbelin
2000-10-04Elimination des coupures sur le type constantherbelin
2000-10-03Ajout castedopenconstrargherbelin
2000-10-03Rebranchement de la tactique Letherbelin
2000-10-01Renommage AppL en Appherbelin
2000-10-01Plus de whd_castappherbelin
2000-10-01Plus de whd_castapp_stackherbelin
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-10Correction pour make docherbelin
2000-09-10Suppression de Abstherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-08-17Pattern matching de sous-termesdelahaye
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-24Passage à des contextes de vars et de rels pouvant contenir des déclaration...herbelin
2000-07-21Pattern -> parsingdelahaye
2000-07-21Modifs d'interpretation de patternsdelahaye
2000-07-20portage Refinefilliatr
2000-07-03Correction de Cofixdelahaye
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-21portage EAuto et Ringfilliatr
2000-06-01Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
2000-05-31Nettoyage de Genericherbelin
2000-05-25Déplacement de save_thm and co de PFedit vers Commandherbelin
2000-05-25Bug existential_value au lieu de existential_type + divers sur existentialherbelin
2000-05-23Docherbelin
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
2000-05-18bug (typage avec meta)herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 02:46:38 +0000