Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-02 04:52:52 -0700 (Mon, 02 May 2005)
Revision: 7243
Log message:

      When a free variable is encountered where a hypothesis type is expected, just
      unify it with "TypeHyp (gensym(), gensym ())" instead of giving up.
      
      Jason, please take a look - is this reasonable?
      

Changes	Path
+12 -11	metaprl/refiner/reflib/term_ty_infer.ml
+0 -2	metaprl/theories/cic/cic_ind_type.ml