Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-23 12:40:17 -0800 (Fri, 23 Dec 2005)
Revision: 8355
Log message:

      This merges Itt_list2!nth with Itt_list3!nth_elem. The new operation is called
      Itt_list2!nth, but is defined the way Itt_list3!nth_elem used to be defined ---
      namely nth{l;2} is unconditionally equal to hd{tl{tl{l}}.
      

Changes  Path
+41 -15 metaprl/theories/itt/core/itt_list2.ml
+9041 -9257 metaprl/theories/itt/core/itt_list2.prla
+15 -38 metaprl/theories/itt/extensions/base/itt_list3.ml
+0 -2 metaprl/theories/itt/extensions/base/itt_list3.mli
+16 -17 metaprl/theories/itt/extensions/base/itt_list3.prla
+1 -1 metaprl/theories/itt/extensions/vector/itt_vec_list1.ml
+1 -2 metaprl/theories/itt/extensions/vector/itt_vec_list1.prla
+9 -9 metaprl/theories/itt/extensions/vector/itt_vec_sequent_term.ml
+4788 -4973 metaprl/theories/itt/extensions/vector/itt_vec_sequent_term.prla
+1 -1 metaprl/theories/itt/reflection/core/itt_hoas_vector.ml
+2 -2 metaprl/theories/itt/reflection/core/itt_hoas_vector.prla
+1949 -2060 metaprl/theories/itt/reflection/experimental/itt_hoas_bterm.prla
+6 -6 metaprl/theories/itt/reflection/experimental/itt_hoas_bterm_wf.ml
+2 -2 metaprl/theories/itt/reflection/experimental/itt_hoas_bterm_wf.prla
+1 -1 metaprl/theories/itt/reflection/experimental/itt_hoas_bterm_wf1.ml
+2 -2 metaprl/theories/itt/reflection/experimental/itt_hoas_bterm_wf1.prla
+2543 -2836 metaprl/theories/itt/reflection/experimental/itt_hoas_lang.prla