Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-10 15:09:14 -0800 (Tue, 10 Jan 2006)
Revision: 8448
Log message:

      Check whether forward-chaining ever produces more than one "main" subgoal.
      
         - Added a new tactical 
           
              checkSubgoalsT : (tactic_arg list -> unit) -> tactic -> tactic
      
           so that it is possible to look at the results of an inference.
      
         - Pass the location to annotation_processors so that we can print
           more informative error messages if necessary.
      
      However, all this does not help, since each step of forward-chaining
      produces exactly one subgoal labeled "main", but we still get multiple
      "main" subgoals after everything is finished.