aboutsummaryrefslogtreecommitdiff
path: root/proofs/tacmach.mli
AgeCommit message (Expand)Author
2000-09-10Ajout d'un LetIn primitif.herbelin
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-21Modifs d'interpretation de patternsdelahaye
2000-06-21portage EAuto et Ringfilliatr
2000-05-16Retrait du i pour tclTHEN_i et correction bugs Decomposeherbelin
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-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
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-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