aboutsummaryrefslogtreecommitdiff
path: root/proofs/tacinterp.ml
AgeCommit message (Expand)Author
2000-09-14Abstraction de constrherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Suppression de Abstherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-08-17Pattern matching de sous-termesdelahaye
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-07-21Modifs d'interpretation de patternsdelahaye
2000-07-20portage Refinefilliatr
2000-06-28Modifs de presentation.delahaye
2000-06-21portage EAuto et Ringfilliatr
2000-06-01Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
2000-05-03compilation bytecode / native :filliatr
2000-05-03Ajout du langage de tactiquesdelahaye
1999-12-07debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesfilliatr
1999-10-22module Macros et Tacinterpfilliatr