Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-17 17:49:50 -0800 (Fri, 17 Feb 2006)
Revision: 8730
Log message:

      Reducing constant inequalities in intro and elim was implemented a bit badly. For
      example, if we had a hyp of the form "1 >= 0", elim would reduce it to
      "assert{bnot{bfalse}}" and a subsequent elim would then eliminate the bnot,
      potentially replacing a provable conclusion with an unprovable
      "assert{bfalse}" (Oops!).