Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-05 17:50:15 -0800 (Sun, 05 Mar 2006)
Revision: 8851
Log message:

      Implemented full fall-back for the intro resource. Now dT 0 will fall back to
      less specific matches if the tactics for the more specific matches fail
      _unless_ the tactic was specifically added as a "last resort" one (using
      "wrap_intro ~fall_through:false").
      

Changes  Path
+34 -28 metaprl/support/tactics/dtactic.ml
+7 -1 metaprl/support/tactics/dtactic.mli
+804 -765 metaprl/theories/itt/applications/algebra/itt_cyclic_group.prla
+7 -4 metaprl/theories/itt/applications/algebra/itt_group.ml
+0 -6 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent.ml