aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Expand)Author
2000-09-26MAJherbelin
2000-09-14MAJherbelin
2000-09-12MAJherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-09-06Canonisation de certains noms dans Pretyping, Asterm et Safe_typingherbelin
2000-07-24MAJherbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-06-21bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> .vo...filliatr
2000-06-02MAJherbelin
2000-06-01Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
2000-05-18MAJ modifs Inductiveherbelin
2000-05-05MAJherbelin
2000-05-04Nettoyage de l'interface de Pfeditherbelin
2000-05-03Ajout de PrintConstr pour debugdelahaye
2000-05-03renommage de certains printersherbelin
2000-04-30MAJherbelin
2000-04-28MAJherbelin
2000-04-17Prise en compte du renommage des fonctions de Asttermherbelin
2000-03-28Nettoyage de l'interface d'Astterm; renommage des {pf_,}constr_of_com* en {pf...herbelin
2000-03-18bug discharge (work_alist contenanti plein de fois les memes choses)filliatr
2000-03-17Correction bug des réduction 'deltat' et renommage 'deltat' en 'evar'herbelin
2000-03-07Renommage ppterm0 --> pptermherbelin
2000-01-26mise a jourfilliatr
2000-01-21gros commit de tout ce que j'ai fait pendant les vacances :filliatr
2000-01-07Restructuration printer et parserherbelin
2000-01-07Restructuration diversesherbelin
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
1999-12-14rattrapage exceptions autres que UserErrorfilliatr
1999-12-14pretty-printers pour le debuggerfilliatr
1999-12-12Ajout pp pattern et rawtermherbelin
1999-12-12modules et coqcfilliatr
1999-12-10indications pour les developpeursfilliatr
1999-12-10debug resetfilliatr
1999-12-05premier debugagefilliatr
1999-12-03renommage pour eviter pbm avec ocamldep (syntax error)filliatr
1999-12-03pour debugger dans le toplevel ocamlfilliatr
1999-12-02Modifs suite à intégration de class.mlherbelin
1999-12-01Intégration du Termast et du Retyping de HH, et modifications connexesherbelin
1999-11-26module Classops; ajout de fonctions dans Declare en consequencefilliatr
1999-11-26style utilise dans le codefilliatr
1999-11-24Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsfilliatr
1999-11-23modules Indrec, Tacentries, Hiddentacfilliatr
1999-11-22module Wcclausenvfilliatr
1999-11-19modules Bij, Gmapl, Stockfilliatr
1999-11-19discriminations netsfilliatr
1999-10-20modules Evar_refiner et Typing_evfilliatr
1999-10-14module Proof_treesfilliatr
1999-10-13mise a jourfilliatr
1999-09-27ajout des constraintes pendant le chargement d'un module (load)filliatr
1999-09-25ensembles de contraintes d'universfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 06:33:00 +0000