Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-02-04 11:38:29 -0800 (Sun, 04 Feb 2001)
Revision: 3139
Log message:

      I moved the bind operator from ITT to the Perv module. This makes sense because
      what we really mean by "bind" is a generic binding construction, not something
      ITT-specific.
      I've also replaced Perv!lambda with Perv!bind since it was now redundant
      and it was indeed used as "bind", not as "lambda" (there were no beta-reduction
      for Perv!lambda).
      

Changes  Path
+1 -1 metaprl/refiner/refiner/refine.ml
+2 -1 metaprl/refiner/refsig/term_man_sig.ml
+8 -6 metaprl/refiner/term_ds/term_man_ds.ml
+5 -4 metaprl/refiner/term_gen/term_man_gen.ml
+1 -2 metaprl/theories/czf/czf_itt_axioms.prla
+3 -2 metaprl/theories/czf/czf_itt_eq.ml
+1 -2 metaprl/theories/czf/czf_itt_eq.prla
+2 -254 metaprl/theories/czf/czf_itt_nat.ml
+1 -2 metaprl/theories/czf/czf_itt_nat.prla
+3 -143 metaprl/theories/czf/czf_itt_power.ml
+1 -2 metaprl/theories/czf/czf_itt_power.prla
+3 -2 metaprl/theories/czf/czf_itt_set.ml
+1 -2 metaprl/theories/czf/czf_itt_set.prla
+5 -4 metaprl/theories/czf/czf_itt_set_ind.ml
+1 -2 metaprl/theories/czf/czf_itt_set_ind.prla
+5 -4 metaprl/theories/itt/itt_bool.ml
+1 -2 metaprl/theories/itt/itt_bool.prla
+6 -6 metaprl/theories/itt/itt_collection.ml
+1 -2 metaprl/theories/itt/itt_collection.prla
+2 -1 metaprl/theories/itt/itt_derive.ml
+1 -2 metaprl/theories/itt/itt_derive.prla
+1 -1 metaprl/theories/itt/itt_dprod.ml
+1 -2 metaprl/theories/itt/itt_dprod_imp.prla
+0 -14 metaprl/theories/itt/itt_equal.ml
+0 -4 metaprl/theories/itt/itt_equal.mli
+4 -4 metaprl/theories/itt/itt_squiggle.ml
+0 -2 metaprl/theories/itt/itt_squiggle.mli
+1 -1 metaprl/theories/itt/itt_squiggle.prla
+4 -9 metaprl/theories/itt/itt_struct.ml
+1 -2 metaprl/theories/itt/itt_struct.prla
+8 -8 metaprl/theories/itt/itt_struct2.ml
+1 -2 metaprl/theories/itt/itt_struct2.prla
+5 -3 metaprl/theories/tactic/perv.ml
+1 -1 metaprl/theories/tactic/perv.mli