aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacticals.ml
AgeCommit message (Expand)Author
2000-11-27Prise en compte des let-in dans les fonctions de réduction pour les tactiquesherbelin
2000-11-02correction Abstract (et make world passe!)filliatr
2000-11-02suppression des (* open Generic *)filliatr
2000-10-18Renommage canonique :herbelin
2000-10-01Renommage AppL en Appherbelin
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éclarationsherbelin
2000-07-21Modifs d'interpretation de patternsdelahaye
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
2000-05-18Effets de bords suite à la restructuration des inductives (cf Inductive)herbelin
2000-05-16Retrait du i pour tclTHEN_i et correction bugs Decomposeherbelin
2000-05-03Encapsulage de PatternMatchingFailure par un 'error' pour que l'echec de conc...herbelin
2000-05-03Ajout du langage de tactiquesdelahaye
2000-04-30Suite intégration de constr_patternherbelin
2000-04-28Déplacement du type reference dans Termherbelin
2000-04-28Changement de représentation du contexte des réf dans rawconstr et patternherbelin
2000-04-26Introduction d'un type constr_pattern pour les différents filtragesherbelin
2000-01-26MAJ ocaml 2.99 (espaces dans la syntaxe des cast)herbelin
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-07debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesfilliatr
1999-12-05premier debugagefilliatr
1999-12-01 - environment -> safe_environmentfilliatr
1999-11-23modules Indrec, Tacentries, Hiddentacfilliatr
1999-11-22module Wcclausenvfilliatr
1999-11-22module Tactics (debut)filliatr
1999-11-19module Pattern, Wcclausenv (interface) et Tacticalsfilliatr