Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-24 05:27:02 -0700 (Thu, 24 Jun 2004)
Revision: 6010
Log message:
This implements the bug 169 RFE - now one can finally just say "open Basic_tactics"
and not worry about having to open all kinds of Refiner.*, Tactic_type.*, Top_*,
etc!
Note that the new support/tactics/basic_tactcs.ml file does not have an .mli
and would not currently compile under make.