Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-26 12:57:46 -0700 (Fri, 26 May 2000)
Revision: 2993
Log message:

       - Fixed a nasty bug in Term_ds.subst - it didn't notice when the same variable
      was mentioned several times in the substitution with different terms substituted
      for it. This made it possible to break Term_ds invariants leading to all kinds of
      strange behaviour.
      
       - Changed the argument order for "subst" to be more natural
      
       - Added a subst1 function to substitute for a single variable without having
      to put the substitution into a singleton list.
      
       - Added the resource annotations and updated the rest of the resource code
      in CZF so that it now compiles (but I didn't try to expand anything).
      

Changes  Path
+1 -1 metaprl/refiner/refiner/refine.ml
+11 -11 metaprl/refiner/reflib/jall.ml
+5 -1 metaprl/refiner/refsig/term_subst_sig.ml
+2 -2 metaprl/refiner/rewrite/rewrite.ml
+4 -4 metaprl/refiner/rewrite/rewrite_build_contractum.ml
+1 -1 metaprl/refiner/rewrite/rewrite_compile_redex.ml
+4 -1 metaprl/refiner/term_ds/term_ds_sig.ml
+22 -10 metaprl/refiner/term_ds/term_subst_ds.ml
+54 -49 metaprl/refiner/term_std/term_subst_std.ml
+21 -72 metaprl/theories/czf/czf_itt_all.ml
+4 -51 metaprl/theories/czf/czf_itt_and.ml
+16 -66 metaprl/theories/czf/czf_itt_dall.ml
+17 -67 metaprl/theories/czf/czf_itt_dexists.ml
+12 -121 metaprl/theories/czf/czf_itt_eq.ml
+20 -75 metaprl/theories/czf/czf_itt_exists.ml
+4 -47 metaprl/theories/czf/czf_itt_false.ml
+0 -1 metaprl/theories/czf/czf_itt_false.mli
+6 -75 metaprl/theories/czf/czf_itt_implies.ml
+3 -22 metaprl/theories/czf/czf_itt_member.ml
+4 -51 metaprl/theories/czf/czf_itt_or.ml
+1 -15 metaprl/theories/czf/czf_itt_rel.ml
+5 -36 metaprl/theories/czf/czf_itt_sall.ml
+11 -45 metaprl/theories/czf/czf_itt_sep.ml
+15 -79 metaprl/theories/czf/czf_itt_set.ml
+41 -52 metaprl/theories/czf/czf_itt_set_ind.ml
+6 -38 metaprl/theories/czf/czf_itt_sexists.ml
+4 -47 metaprl/theories/czf/czf_itt_true.ml
+4 -39 metaprl/theories/czf/czf_itt_union.ml
+1 -1 metaprl/theories/itt/itt_dprod.ml
+2 -2 metaprl/theories/itt/itt_int.ml
+2 -2 metaprl/theories/itt/itt_rfun.ml
+1 -1 metaprl/theories/itt/itt_w.ml
+2 -2 metaprl/theories/tactic/tactic_cache.ml
+2 -2 metaprl/theories/tptp/tptp_prove.ml