Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-07 17:52:36 -0700 (Wed, 07 May 2003)
Revision: 4574
Log message:

      Added a few helper functions for the case we need to pass two terms to an intro
      or elim rule and the first one can be typeinf'ed.
      

Changes  Path
+2 -0 metaprl/support/tactics/dtactic.ml
+2 -0 metaprl/support/tactics/dtactic.mli
+6 -0 metaprl/support/tactics/typeinf.ml
+1 -0 metaprl/support/tactics/typeinf.mli
+1 -1 metaprl/util/check-status