aboutsummaryrefslogtreecommitdiff
path: root/tactics/wcclausenv.mli
AgeCommit message (Expand)Author
2003-10-11Death of 'a somewhat cryptic module'herbelin
2003-10-10Dead of 'a somewhat cryptic module' (Inv doesn't use applyUsing any longer; p...herbelin
2002-12-19suite du commit precedentbarras
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-11-19Diverses petites simplications de la machine de preuves.clrenard
2001-11-12Suppression des stamps et donc des *_constraintsclrenard
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
2001-03-28amelioration de la structure des universbarras
2001-03-15entetesfilliatr
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
2000-05-16Retrait du i pour tclTHEN_i et correction bugs Decomposeherbelin
2000-05-03Ajout du langage de tactiquesdelahaye
2000-01-21gros commit de tout ce que j'ai fait pendant les vacances :filliatr
1999-11-25typage des existentielles dans Typing_ev; suppression metamap inutiles dans t...filliatr
1999-11-24Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsfilliatr
1999-11-22module Wcclausenvfilliatr
1999-11-19module Pattern, Wcclausenv (interface) et Tacticalsfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:25:32 +0000