aboutsummaryrefslogtreecommitdiff
path: root/proofs/pfedit.ml
AgeCommit message (Expand)Author
2000-12-12Hint Unfold Local + commentairesmohring
2000-11-23print_id, print_sp -> pr_id, pr_spherbelin
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-09-10Correction pour make docherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-05-25Déplacement de save_thm and co de PFedit vers Commandherbelin
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
2000-05-05Achèvement nettoyage Pfeditherbelin
2000-05-04Nettoyage de l'interface de Pfeditherbelin
2000-05-03Ajout du langage de tactiquesdelahaye
2000-03-28Nettoyage de l'interface d'Astterm; renommage des {pf_,}constr_of_com* en {pf...herbelin
1999-12-14rattrapage exceptions autres que UserErrorfilliatr
1999-12-13 - méthode load sur les Hintsfilliatr
1999-12-10 - erreurs Pretypefilliatr
1999-12-10debug resetfilliatr
1999-12-09 - constantes avec recettesfilliatr
1999-12-08deplacement de Discharge dans toplevelfilliatr
1999-12-05premier debugagefilliatr
1999-12-02Pfedit (fin)filliatr
1999-12-01poursuite de Vernacentriesfilliatr
1999-12-01module Pfeditfilliatr