aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticals.mli
Commit message (Expand)AuthorAge
* application patch Cuit Alvarado : tclTHENSi et intros_until_n exportésGravatar filliatr2001-02-01
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Renommage canonique :Gravatar herbelin2000-10-18
* retablissement make doc et make minicoqGravatar filliatr2000-07-25
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Modifs d'interpretation de patternsGravatar delahaye2000-07-21
* Retrait du i pour tclTHEN_i et correction bugs DecomposeGravatar herbelin2000-05-16
* diverses modifs pour ocamlwebGravatar filliatr2000-05-03
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Suite intégration de constr_patternGravatar herbelin2000-04-30
* Déplacement du type reference dans TermGravatar herbelin2000-04-28
* Changement de représentation du contexte des réf dans rawconstr et patternGravatar herbelin2000-04-28
* Introduction d'un type constr_pattern pour les différents filtragesGravatar herbelin2000-04-26
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* documentationGravatar filliatr1999-12-13
* debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesGravatar filliatr1999-12-07
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
* module Tactics (debut)Gravatar filliatr1999-11-22
* module Pattern, Wcclausenv (interface) et TacticalsGravatar filliatr1999-11-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 21:48:34 +0000