Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-01-31 13:42:08 -0800 (Sun, 31 Jan 1999)
Revision: 2580
Log message:

      Added "simp" and "verb" rules to Makefiles.  There are no *.mlp and *.mlip
      files in the refiner any longer.  Instead, the C-preprocessor is run at
      compile time.
      
      By default, the verbose refiner is generated.  To get the others, use
      make simp, or make opt_simp.
      

Changes  Path
+32 -15 metaprl/Makefile
Binary metaprl/editor/emacs/caml-fa.elc
Properties metaprl/editor/emacs/caml-fa.elc
Binary metaprl/editor/emacs/caml-util.elc
Properties metaprl/editor/emacs/caml-util.elc
Binary metaprl/editor/emacs/caml.elc
Properties metaprl/editor/emacs/caml.elc
+1 -1 metaprl/editor/ml/proof.ml
+1 -1 metaprl/editor/ml/proof.mli
+8 -8 metaprl/filter/filter_cache.ml
+40 -33 metaprl/mk/config
+24 -12 metaprl/mk/preface
+3 -8 metaprl/refiner/refiner/Files
+12 -11 metaprl/refiner/refiner/Makefile
Added metaprl/refiner/refiner/refine.ml
Properties metaprl/refiner/refiner/refine.ml
Added metaprl/refiner/refiner/refine.mli
Properties metaprl/refiner/refiner/refine.mli
Deleted metaprl/refiner/refiner/refine.mlip
Deleted metaprl/refiner/refiner/refine.mlp
Added metaprl/refiner/refiner/refiner_ds.ml
Properties metaprl/refiner/refiner/refiner_ds.ml
Added metaprl/refiner/refiner/refiner_ds.mli
Properties metaprl/refiner/refiner/refiner_ds.mli
Deleted metaprl/refiner/refiner/refiner_ds_simp.ml
Deleted metaprl/refiner/refiner/refiner_ds_simp.mli
Deleted metaprl/refiner/refiner/refiner_ds_verb.ml
Deleted metaprl/refiner/refiner/refiner_ds_verb.mli
Added metaprl/refiner/refiner/refiner_std.ml
Properties metaprl/refiner/refiner/refiner_std.ml
Added metaprl/refiner/refiner/refiner_std.mli
Properties metaprl/refiner/refiner/refiner_std.mli
Deleted metaprl/refiner/refiner/refiner_std_simp.ml
Deleted metaprl/refiner/refiner/refiner_std_simp.mli
Deleted metaprl/refiner/refiner/refiner_std_verb.ml
Deleted metaprl/refiner/refiner/refiner_std_verb.mli
+4 -4 metaprl/refiner/reflib/Files
+6 -6 metaprl/refiner/reflib/ml_term.ml
+6 -6 metaprl/refiner/reflib/term_copy.ml
+12 -12 metaprl/refiner/reflib/term_copy.mli
+5 -5 metaprl/refiner/reflib/term_copy2.ml
+12 -12 metaprl/refiner/reflib/term_copy2.mli
+7 -3 metaprl/refiner/refsig/refine_error.h
+9 -12 metaprl/refiner/rewrite/Files
+2 -0 metaprl/refiner/rewrite/Makefile
Added metaprl/refiner/rewrite/rewrite.ml
Properties metaprl/refiner/rewrite/rewrite.ml
Added metaprl/refiner/rewrite/rewrite.mli
Properties metaprl/refiner/rewrite/rewrite.mli
Deleted metaprl/refiner/rewrite/rewrite.mlip
Deleted metaprl/refiner/rewrite/rewrite.mlp
Added metaprl/refiner/rewrite/rewrite_build_contractum.ml
Properties metaprl/refiner/rewrite/rewrite_build_contractum.ml
Added metaprl/refiner/rewrite/rewrite_build_contractum.mli
Properties metaprl/refiner/rewrite/rewrite_build_contractum.mli
Deleted metaprl/refiner/rewrite/rewrite_build_contractum.mlip
Deleted metaprl/refiner/rewrite/rewrite_build_contractum.mlp
Added metaprl/refiner/rewrite/rewrite_compile_contractum.ml
Properties metaprl/refiner/rewrite/rewrite_compile_contractum.ml
Added metaprl/refiner/rewrite/rewrite_compile_contractum.mli
Properties metaprl/refiner/rewrite/rewrite_compile_contractum.mli
Deleted metaprl/refiner/rewrite/rewrite_compile_contractum.mlip
Deleted metaprl/refiner/rewrite/rewrite_compile_contractum.mlp
Added metaprl/refiner/rewrite/rewrite_compile_redex.ml
Properties metaprl/refiner/rewrite/rewrite_compile_redex.ml
Added metaprl/refiner/rewrite/rewrite_compile_redex.mli
Properties metaprl/refiner/rewrite/rewrite_compile_redex.mli
Deleted metaprl/refiner/rewrite/rewrite_compile_redex.mlip
Deleted metaprl/refiner/rewrite/rewrite_compile_redex.mlp
Added metaprl/refiner/rewrite/rewrite_debug.ml
Properties metaprl/refiner/rewrite/rewrite_debug.ml
Added metaprl/refiner/rewrite/rewrite_debug.mli
Properties metaprl/refiner/rewrite/rewrite_debug.mli
Deleted metaprl/refiner/rewrite/rewrite_debug.mlip
Deleted metaprl/refiner/rewrite/rewrite_debug.mlp
Added metaprl/refiner/rewrite/rewrite_match_redex.ml
Properties metaprl/refiner/rewrite/rewrite_match_redex.ml
Added metaprl/refiner/rewrite/rewrite_match_redex.mli
Properties metaprl/refiner/rewrite/rewrite_match_redex.mli
Deleted metaprl/refiner/rewrite/rewrite_match_redex.mlip
Deleted metaprl/refiner/rewrite/rewrite_match_redex.mlp
Added metaprl/refiner/rewrite/rewrite_meta.ml
Properties metaprl/refiner/rewrite/rewrite_meta.ml
Added metaprl/refiner/rewrite/rewrite_meta.mli
Properties metaprl/refiner/rewrite/rewrite_meta.mli
Deleted metaprl/refiner/rewrite/rewrite_meta.mlip
Deleted metaprl/refiner/rewrite/rewrite_meta.mlp
Deleted metaprl/refiner/rewrite/rewrite_type.mlip
Deleted metaprl/refiner/rewrite/rewrite_type.mlp
Added metaprl/refiner/rewrite/rewrite_types.ml
Properties metaprl/refiner/rewrite/rewrite_types.ml
Added metaprl/refiner/rewrite/rewrite_types.mli
Properties metaprl/refiner/rewrite/rewrite_types.mli
Added metaprl/refiner/rewrite/rewrite_util.ml
Properties metaprl/refiner/rewrite/rewrite_util.ml
Added metaprl/refiner/rewrite/rewrite_util.mli
Properties metaprl/refiner/rewrite/rewrite_util.mli
Deleted metaprl/refiner/rewrite/rewrite_util.mlip
Deleted metaprl/refiner/rewrite/rewrite_util.mlp
+3 -6 metaprl/refiner/term_ds/Files
+2 -0 metaprl/refiner/term_ds/Makefile
Added metaprl/refiner/term_ds/term_addr_ds.ml
Properties metaprl/refiner/term_ds/term_addr_ds.ml
Added metaprl/refiner/term_ds/term_addr_ds.mli
Properties metaprl/refiner/term_ds/term_addr_ds.mli
Deleted metaprl/refiner/term_ds/term_addr_ds.mlip
Deleted metaprl/refiner/term_ds/term_addr_ds.mlp
Added metaprl/refiner/term_ds/term_base_ds.ml
Properties metaprl/refiner/term_ds/term_base_ds.ml
Added metaprl/refiner/term_ds/term_base_ds.mli
Properties metaprl/refiner/term_ds/term_base_ds.mli
Deleted metaprl/refiner/term_ds/term_base_ds.mlip
Deleted metaprl/refiner/term_ds/term_base_ds.mlp
Added metaprl/refiner/term_ds/term_eval_ds.ml
Properties metaprl/refiner/term_ds/term_eval_ds.ml
Added metaprl/refiner/term_ds/term_eval_ds.mli
Properties metaprl/refiner/term_ds/term_eval_ds.mli
Deleted metaprl/refiner/term_ds/term_eval_ds.mlip
Deleted metaprl/refiner/term_ds/term_eval_ds.mlp
Added metaprl/refiner/term_ds/term_man_ds.ml
Properties metaprl/refiner/term_ds/term_man_ds.ml
Added metaprl/refiner/term_ds/term_man_ds.mli
Properties metaprl/refiner/term_ds/term_man_ds.mli
Deleted metaprl/refiner/term_ds/term_man_ds.mlip
Deleted metaprl/refiner/term_ds/term_man_ds.mlp
Added metaprl/refiner/term_ds/term_op_ds.ml
Properties metaprl/refiner/term_ds/term_op_ds.ml
Added metaprl/refiner/term_ds/term_op_ds.mli
Properties metaprl/refiner/term_ds/term_op_ds.mli
Deleted metaprl/refiner/term_ds/term_op_ds.mlip
Deleted metaprl/refiner/term_ds/term_op_ds.mlp
Added metaprl/refiner/term_ds/term_subst_ds.ml
Properties metaprl/refiner/term_ds/term_subst_ds.ml
Added metaprl/refiner/term_ds/term_subst_ds.mli
Properties metaprl/refiner/term_ds/term_subst_ds.mli
Deleted metaprl/refiner/term_ds/term_subst_ds.mlip
Deleted metaprl/refiner/term_ds/term_subst_ds.mlp
+1 -4 metaprl/refiner/term_gen/Files
+2 -0 metaprl/refiner/term_gen/Makefile
Added metaprl/refiner/term_gen/term_addr_gen.ml
Properties metaprl/refiner/term_gen/term_addr_gen.ml
Added metaprl/refiner/term_gen/term_addr_gen.mli
Properties metaprl/refiner/term_gen/term_addr_gen.mli
Deleted metaprl/refiner/term_gen/term_addr_gen.mlip
Deleted metaprl/refiner/term_gen/term_addr_gen.mlp
Added metaprl/refiner/term_gen/term_man_gen.ml
Properties metaprl/refiner/term_gen/term_man_gen.ml
Added metaprl/refiner/term_gen/term_man_gen.mli
Properties metaprl/refiner/term_gen/term_man_gen.mli
Deleted metaprl/refiner/term_gen/term_man_gen.mlip
Deleted metaprl/refiner/term_gen/term_man_gen.mlp
Added metaprl/refiner/term_gen/term_meta_gen.ml
Properties metaprl/refiner/term_gen/term_meta_gen.ml
Added metaprl/refiner/term_gen/term_meta_gen.mli
Properties metaprl/refiner/term_gen/term_meta_gen.mli
Deleted metaprl/refiner/term_gen/term_meta_gen.mlip
Deleted metaprl/refiner/term_gen/term_meta_gen.mlp
Added metaprl/refiner/term_gen/term_shape_gen.ml
Properties metaprl/refiner/term_gen/term_shape_gen.ml
Added metaprl/refiner/term_gen/term_shape_gen.mli
Properties metaprl/refiner/term_gen/term_shape_gen.mli
Deleted metaprl/refiner/term_gen/term_shape_gen.mlip
Deleted metaprl/refiner/term_gen/term_shape_gen.mlp
+3 -6 metaprl/refiner/term_std/Files
+2 -0 metaprl/refiner/term_std/Makefile
Added metaprl/refiner/term_std/term_base_std.ml
Properties metaprl/refiner/term_std/term_base_std.ml
Added metaprl/refiner/term_std/term_base_std.mli
Properties metaprl/refiner/term_std/term_base_std.mli
Deleted metaprl/refiner/term_std/term_base_std.mlip
Deleted metaprl/refiner/term_std/term_base_std.mlp
Added metaprl/refiner/term_std/term_eval_std.ml
Properties metaprl/refiner/term_std/term_eval_std.ml
Added metaprl/refiner/term_std/term_eval_std.mli
Properties metaprl/refiner/term_std/term_eval_std.mli
Deleted metaprl/refiner/term_std/term_eval_std.mlip
Deleted metaprl/refiner/term_std/term_eval_std.mlp
Added metaprl/refiner/term_std/term_op_std.ml
Properties metaprl/refiner/term_std/term_op_std.ml
Added metaprl/refiner/term_std/term_op_std.mli
Properties metaprl/refiner/term_std/term_op_std.mli
Deleted metaprl/refiner/term_std/term_op_std.mlip
Deleted metaprl/refiner/term_std/term_op_std.mlp
Added metaprl/refiner/term_std/term_subst_std.ml
Properties metaprl/refiner/term_std/term_subst_std.ml
Added metaprl/refiner/term_std/term_subst_std.mli
Properties metaprl/refiner/term_std/term_subst_std.mli
Deleted metaprl/refiner/term_std/term_subst_std.mlip
Deleted metaprl/refiner/term_std/term_subst_std.mlp