Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-28 00:48:10 -0700 (Mon, 28 Jul 2003)
Revision: 4780
Log message:

      - Now one can use withT to tell JProver with term to use as a canonical
      element of types (JProver presumes all types to be non-empty) instead
      of the default << 'v0_jprover >>.
      - Killed some of the debugging printouts in JProver.
      

Changes  Path
+19 -19 metaprl/refiner/reflib/jall.ml
+2 -1 metaprl/theories/itt/itt_logic.ml
+20 -20 metaprl/theories/itt/jprover_tests.ml
+360 -358 metaprl/theories/itt/jprover_tests.prla