Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-07-13 11:45:39 -0700 (Tue, 13 Jul 2004)
Revision: 6070
Log message:

      - Removed the "reduce" annotation that was preventing MetaPRL from starting.
      - Formatted the commen ts and code a bit more consistently.
      - In subst, the bterm that is being substituted must be simple (this is necessary
      because we may allow combining nested bterm operators).
      

Changes	Path
+76 -70	metaprl/theories/base/base_reflection.ml