Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-23 17:26:12 -0800 (Sun, 23 Jan 2005)
Revision: 6478
Log message:

      Make the Term_grammar produce terms of type "parsed_term", which
      is an abstract type.  This forces us to to do a term_of_parsed_term
      and a type check before getting a real term.
      
      All proofs still check.
      

Changes	Path
+1 -1	metaprl-branches/opname_classes2/filter/base/filter_magic.ml
+3 -3	metaprl-branches/opname_classes2/filter/base/filter_summary.ml
+34 -29	metaprl-branches/opname_classes2/filter/base/filter_type.ml
+7 -11	metaprl-branches/opname_classes2/filter/base/filter_util.ml
+1 -3	metaprl-branches/opname_classes2/filter/base/filter_util.mli
+436 -357	metaprl-branches/opname_classes2/filter/filter/filter_parse.ml
+4 -1	metaprl-branches/opname_classes2/filter/filter/filter_patt.ml
+4 -2	metaprl-branches/opname_classes2/filter/filter/filter_prog.ml
+68 -50	metaprl-branches/opname_classes2/filter/filter/term_grammar.ml
+4 -3	metaprl-branches/opname_classes2/filter/filter/term_grammar.mli
+10 -17	metaprl-branches/opname_classes2/refiner/refbase/opname.ml
+1 -1	metaprl-branches/opname_classes2/refiner/refiner/refiner_ds.ml
+1 -1	metaprl-branches/opname_classes2/refiner/refiner/refiner_std.ml
+16 -23	metaprl-branches/opname_classes2/refiner/reflib/term_ty_infer.ml
+1 -1	metaprl-branches/opname_classes2/refiner/refsig/refiner_sig.ml
+6 -6	metaprl-branches/opname_classes2/refiner/refsig/term_ty_sig.ml
+1 -1	metaprl-branches/opname_classes2/refiner/term_gen/term_ty_gen.ml
+21 -0	metaprl-branches/opname_classes2/support/shell/package_info.ml
+5 -2	metaprl-branches/opname_classes2/support/shell/package_info.mli
+2 -2	metaprl-branches/opname_classes2/support/shell/shell_core.ml
+41 -11	metaprl-branches/opname_classes2/support/shell/shell_state.ml
+3 -2	metaprl-branches/opname_classes2/support/shell/shell_state.mli