Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-29 08:23:04 -0700 (Thu, 29 Sep 2005)
Revision: 7802
Log message:

      Implemented the type-sensitive interpretation of binding contexts. Now 
      
      arg{| <H> >- 'C |}
      
      that is currently parsed as
      
      arg{| <H<||>[]> >- 'C<|H|>[] |}
      
      will get parsed as
      
      arg{| <H<||>[]> >- 'C<||>[] |}
      
      (i.e. 'C no longer depends on H) when arg is declared as
      
      declare sequent [arg] { Ignore : ... >- ...} : ...
      `
      

Changes  Path
+6 -0 metaprl/filter/base/filter_cache_fun.ml
+1 -1 metaprl/filter/base/filter_magic.ml
+2 -1 metaprl/filter/base/filter_type.ml
+6 -6 metaprl/filter/filter/filter_parse.ml
+23 -14 metaprl/filter/filter/term_grammar.ml
+27 -21 metaprl/refiner/refiner/refiner_debug.ml
+2 -2 metaprl/refiner/reflib/ascii_io.ml
+7 -0 metaprl/refiner/reflib/term_ty_infer.ml
+5 -0 metaprl/refiner/reflib/term_ty_infer.mli
+8 -5 metaprl/refiner/refsig/term_meta_sig.ml
+2 -2 metaprl/refiner/refsig/termmod_sig.ml
+43 -37 metaprl/refiner/term_gen/term_meta_gen.ml
+0 -16 metaprl/support/display/perv.ml
+27 -27 metaprl/theories/ilc/ilc_core.ml
+20 -20 metaprl/theories/ilc/ilc_extend.ml
+1 -1 metaprl/theories/ilc/ilc_test.ml
+40 -40 metaprl/theories/s4lp/s4_logic.ml
+1 -1 metaprl/util/gen_refiner_debug.pl