NEWS * New method metisFT: A version of metis that uses full type information in order to avoid failures of proof reconstruction.
It hasn't been tested much. Ultimately, the idea is to incorporate it into Metis itself so that it is called automatically if the untyped version raises an exception. Larry
