aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.mllib
Commit message (Expand)AuthorAge
* Made the side-conditions of lemmas always come last when chaining "apply in"Gravatar herbelin2009-12-13
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Fixing bug #2308 ("instantiate" tactic did not comply withGravatar herbelin2009-04-24
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20