Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-08 00:04:25 -0800 (Tue, 08 Feb 2005)
Revision: 6629
Log message:

      I overlooked free type variables in the environment during existential
      quantification in rules and rewrites.  This fixes it.  However, note
      that rewrites like the following don't typecheck.
      
         prim_rw add_sub_one :
            ('a in int) -->
            'a <--> (('a +@ 1) -@ 1)
      
      The rewrite is quite sensible in Itt, but problematic because it
      applies to any term in the system (including display forms
      for example).  The quick solution is to add the constraint.
      
         prim_rw add_sub_one ('a :> Term) :
            ('a in int) -->
            'a <--> (('a +@ 1) -@ 1)
      
      This is a bit suboptimal, but rewrites like this are very rare,
      and the extra alpha-equality adds only O(1) overhead.
      

Changes  Path
+12 -7 metaprl/filter/base/filter_cache_fun.ml
+2 -0 metaprl/filter/base/filter_type.ml
+1 -1 metaprl/filter/filter/filter_parse.ml
+4 -2 metaprl/filter/filter/term_grammar.ml
+59 -43 metaprl/refiner/reflib/term_ty_infer.ml
+1 -0 metaprl/refiner/reflib/term_ty_infer.mli
+2 -3 metaprl/theories/base/base_rewrite.ml
+1 -1 metaprl/theories/base/base_rewrite.mli
+7 -6 metaprl/theories/itt/itt_int_base.ml
+2 -2 metaprl/theories/itt/itt_int_ext.ml
+1 -1 metaprl/theories/itt/itt_int_ext.prla
+6 -6 metaprl/theories/itt/itt_rat.ml
+2 -2 metaprl/theories/itt/itt_record_renaming.ml
+2 -1 metaprl/theories/itt/itt_reflection.ml
+1 -0 metaprl/theories/itt/itt_reflection.mli
+2 -2 metaprl/theories/itt/itt_reflection.prla
+149 -5 metaprl/theories/ocaml_doc/ocaml_doc_exn1.ml
+1 -1 metaprl/theories/ocaml_doc/ocaml_doc_expr4.ml
+1 -1 mpcompiler/mmc/base/mmc_base_standardize.ml
+0 -6 mpcompiler/mmc/core/mmc_core_cps.ml
+0 -6 mpcompiler/mmc/core/mmc_core_grammar.ml
+1 -1 mpcompiler/mmc/core/mmc_core_type_infer.ml