aboutsummaryrefslogtreecommitdiff
path: root/tactics/tactics.mli
AgeCommit message (Expand)Author
2001-03-15entetesfilliatr
2001-03-01backtrack unification types et deplacement make_clenv_bindingfilliatr
2001-02-01application patch Cuit Alvarado : tclTHENSi et intros_until_n exportésfilliatr
2001-01-31Mise en place de la possibilite d'unfolder des variables locales et des const...filliatr
2001-01-24Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...herbelin
2000-12-18Renommages autour de NewInductionherbelin
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-11-26Distinction claire entre Induction (nom interne : raw_induct) et le nouvel in...herbelin
2000-11-24Nouveau choix pour l'intros initialdelahaye
2000-10-18Renommage canonique :herbelin
2000-10-13Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...herbelin
2000-09-10nettoyageherbelin
2000-09-10Suppression de Abstherbelin
2000-05-16Retrait du i pour tclTHEN_i et correction bugs Decomposeherbelin
2000-05-05Achèvement nettoyage Pfedit; ajout intros_replacingherbelin
2000-05-04Nettoyage de l'interface de Pfeditherbelin
2000-05-03Ajout du langage de tactiquesdelahaye
1999-12-03modules profile, Coqinit et Coqtop (=main)filliatr
1999-12-02modifs pour premiere edition de liensfilliatr
1999-11-22module Tactics (debut)filliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 08:20:35 +0000