aboutsummaryrefslogtreecommitdiff
path: root/proofs/logic.ml
AgeCommit message (Expand)Author
2001-10-05Petit oubli à propos de ThinBodyherbelin
2001-10-05Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...herbelin
2001-08-08Ajout nf_betaiota dans le cut interneherbelin
2001-08-07Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...herbelin
2001-06-25Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...herbelin
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
2001-05-03Changement de la structure des points fixesbarras
2001-04-14Reparation du bug de Trydelahaye
2001-03-28amelioration de la structure des universbarras
2001-03-15entetesfilliatr
2001-02-28introduction d'un refine avec resolution des types et de l'instantiation des ...mohring
2001-02-01*** empty log message ***mohring
2000-12-06Ajout erreur DoesNotOccurInherbelin
2000-11-23print_id, print_sp -> pr_id, pr_spherbelin
2000-11-02correction Abstract (et make world passe!)filliatr
2000-11-02suppression des (* open Generic *)filliatr
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
2000-10-18Renommage canonique :herbelin
2000-10-11Renommage des find_m*typeherbelin
2000-10-05Suppression d'un Cast inutileherbelin
2000-10-04Ajout LetIn dans prim_extractorherbelin
2000-10-03Rebranchement de la tactique Letherbelin
2000-10-01Renommage AppL en Appherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 16:06:23 +0000