Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-04-30 12:32:04 -0700 (Fri, 30 Apr 2004)
Revision: 5744
Log message:

      mpconfig - theories/cic was not present in INCLUDES
      var - var_subst_to_bind2 added
      cic_lambda - dfun renamed to fun
      cic_ind_type - bugfixes and some basic automation added
      cic_list - nil_wf and cons_wf proved.
      
      TODO:
      1.Prove well-formedness of the inductive definition of List (list_wf, nil_wf, cons_wf proved)
      2.Destructors & fixpoint for inductive definitions
      

Changes	Path
+1 -0	metaprl/editor/ml/mpconfig
+12 -1	metaprl/support/tactics/var.ml
+6 -0	metaprl/support/tactics/var.mli