aboutsummaryrefslogtreecommitdiff
path: root/proofs/logic.ml
AgeCommit message (Expand)Author
2000-10-01Plus de whd_castappherbelin
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-07-24Passage à des contextes de vars et de rels pouvant contenir des déclaration...herbelin
2000-07-03Correction de Cofixdelahaye
2000-07-01Extension de find_inductive aux co-inductifs et renommage en find_rectypeherbelin
2000-06-29Rienherbelin
2000-05-31Nettoyage de Genericherbelin
2000-05-18Effets de bords suite à la restructuration des inductives (cf Inductive)herbelin
2000-05-04Nettoyage de l'interface de Pfeditherbelin
2000-05-03Ajout du langage de tactiquesdelahaye
2000-04-20Abstraction du type typed_type (un pas vers les jugements 2 niveaux)herbelin
2000-03-21Modification de type_of_case, type_case_branches, etcherbelin
2000-01-26Abstraction de l'implémentation des signatures de Sign en vue intégration d...herbelin
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
1999-12-14rattrapage exceptions autres que UserErrorfilliatr
1999-12-02modifs pour premiere edition de liensfilliatr
1999-12-01module Pfeditfilliatr
1999-12-01 - environment -> safe_environmentfilliatr
1999-12-01 - Typing -> Safe_typingfilliatr
1999-11-25Backtrack sur modif Evd.evd_conclherbelin
1999-11-24MAJ pour fusion avec pretypingherbelin
1999-11-22module Wcclausenvfilliatr
1999-11-22module Tactics (debut)filliatr
1999-11-19module Pattern, Wcclausenv (interface) et Tacticalsfilliatr
1999-10-20module Clenv (debut)filliatr
1999-10-20modules Evar_refiner et Typing_evfilliatr
1999-10-19les variables existentielles contiennent maintenant un environnement (typefilliatr
1999-10-18 - déplacement (encore une fois !) des variables existentielles : elles sontfilliatr
1999-10-14module Logicfilliatr
1999-10-08module Logic (ne compile pas encore)filliatr