Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-05-20 16:03:12 -0700 (Thu, 20 May 1999)
Revision: 2659
Log message:

      - Fixed a bug in Term_ds:
      The code responsible for renaming bound variables was lost during code reorganization in the
      revision 1.34 of term_base_ds.mlp on 1998/12/30
      
      - Fixed a bug in Term_ds and Term_std:
      Functon match_terms never checked if the matched term on the right-hand side had any
      improperly bound variables. As a result,
      match_terms [] <<lambda{y.('f 'y)}>> <<lambda{x.('x 'x)}>>
      was returning
      Refiner.Refiner.TermSubst.term_subst = ["f", x]
      instead of raising an exception
      
      - Some file headers still had "This file is part of Nuprl-Light" instead of
      "This file is part of MetaPRL" - fixed
      

Changes  Path
+1 -1 metaprl/ensemble/appl_ensemble.ml
+1 -1 metaprl/ensemble/appl_ensemble.mli
+1 -1 metaprl/ensemble/appl_outboard_client.ml
+1 -1 metaprl/ensemble/appl_outboard_client.mli
+1 -1 metaprl/ensemble/appl_outboard_common.ml
+1 -1 metaprl/ensemble/appl_outboard_common.mli
+1 -1 metaprl/ensemble/appl_outboard_server.ml
+1 -1 metaprl/ensemble/appl_outboard_server.mli
+1 -1 metaprl/mllib/infinite_weak_array.ml
+1 -1 metaprl/mllib/infinite_weak_array.mli
+1 -1 metaprl/mllib/infinite_weak_array_sig.mlz
+1 -1 metaprl/mllib/int_util.ml
+4 -0 metaprl/mllib/list_util.ml
+1 -0 metaprl/mllib/list_util.mli
+1 -1 metaprl/mllib/marshal_shared.mli
+1 -1 metaprl/mllib/mmap.ml
+1 -1 metaprl/mllib/mmap.mli
+1 -1 metaprl/mllib/mmap_pipe.ml
+1 -1 metaprl/mllib/mmap_pipe.mli
+1 -1 metaprl/mllib/mp_id.ml
+1 -1 metaprl/mllib/simplehash_sig.ml
+1 -1 metaprl/mllib/simplehashtbl.ml
+1 -1 metaprl/mllib/simplehashtbl.mli
+1 -1 metaprl/mllib/weak_memo.ml
+1 -1 metaprl/mllib/weak_memo.mli
+1 -1 metaprl/mllib/weak_memo_sig.ml
+14 -11 metaprl/refiner/reflib/dform_print.ml
+1 -1 metaprl/refiner/reflib/term_compare.ml
+1 -1 metaprl/refiner/reflib/term_compare.mli
+1 -1 metaprl/refiner/reflib/term_compare_sig.ml
+1 -1 metaprl/refiner/reflib/term_copy2_weak.ml
+1 -1 metaprl/refiner/reflib/term_copy2_weak.mli
+1 -1 metaprl/refiner/reflib/term_copy_weak.ml
+1 -1 metaprl/refiner/reflib/term_copy_weak.mli
+1 -1 metaprl/refiner/reflib/term_io.ml
+1 -1 metaprl/refiner/reflib/term_io.mli
+1 -1 metaprl/refiner/refsig/term_hash_sig.ml
+1 -1 metaprl/refiner/refsig/term_header_sig.mlz
+1 -1 metaprl/refiner/refsig/term_norm_sig.ml
+55 -30 metaprl/refiner/term_ds/term_base_ds.ml
+17 -13 metaprl/refiner/term_ds/term_subst_ds.ml
+1 -1 metaprl/refiner/term_gen/term_hash.ml
+1 -1 metaprl/refiner/term_gen/term_hash.mli
+1 -1 metaprl/refiner/term_gen/term_header.ml
+1 -1 metaprl/refiner/term_gen/term_header.mli
+1 -1 metaprl/refiner/term_gen/term_header_constr.ml
+1 -1 metaprl/refiner/term_gen/term_header_constr.mli
+1 -1 metaprl/refiner/term_gen/term_norm.ml
+1 -1 metaprl/refiner/term_gen/term_norm.mli
+13 -5 metaprl/refiner/term_std/term_subst_std.ml
+1 -1 metaprl/theories/fol/fol_all_itt.ml
+1 -1 metaprl/theories/fol/fol_all_itt.mli
+1 -1 metaprl/theories/fol/fol_bisect_itt.ml
+1 -1 metaprl/theories/fol/fol_bisect_itt.mli
+1 -1 metaprl/theories/fol/fol_type_itt.ml
+1 -1 metaprl/theories/fol/fol_type_itt.mli
+1 -1 metaprl/theories/fol/fol_univ_itt.ml
+1 -1 metaprl/theories/fol/fol_univ_itt.mli
+1 -1 metaprl/theories/itt/itt_atom_bool.ml
+1 -1 metaprl/theories/itt/itt_atom_bool.mli
+1 -1 metaprl/theories/itt/itt_bisect.ml
+1 -1 metaprl/theories/itt/itt_bisect.mli
+1 -1 metaprl/theories/itt/itt_bunion.ml
+1 -1 metaprl/theories/itt/itt_bunion.mli
+1 -1 metaprl/theories/itt/itt_list2.ml
+1 -1 metaprl/theories/itt/itt_list2.mli
+1 -1 metaprl/theories/itt/itt_tsub.ml
+1 -1 metaprl/theories/itt/itt_tsub.mli
+1 -1 metaprl/theories/itt/itt_tunion.ml
+1 -1 metaprl/theories/itt/itt_tunion.mli
+1 -1 metaprl/theories/reflect_itt/refl_var.ml
+1 -1 metaprl/theories/reflect_itt/refl_var.mli
+1 -1 metaprl/theories/reflect_itt/refl_var_set.ml
+1 -1 metaprl/theories/reflect_itt/refl_var_set.mli
+1 -1 metaprl/theories/tactic/pre_tactic_type.mli
+1 -1 metaprl/theories/tactic/tacticals.ml