Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-04 14:51:58 -0700 (Fri, 04 Jul 2003)
Revision: 4701
Log message:

      Explode_term must be a total function (we can not have tactics using
      it raise Invalid_argument just because they happen to hit an unsupported
      parameter).
      

Changes  Path
+1 -0 metaprl/refiner/refsig/term_sig.ml
+1 -1 metaprl/refiner/term_ds/term_base_ds.ml
+1 -0 metaprl/refiner/term_ds/term_ds.ml
+1 -0 metaprl/refiner/term_ds/term_ds_sig.ml
+1 -1 metaprl/refiner/term_std/term_base_std.ml
+1 -0 metaprl/refiner/term_std/term_std.ml
+1 -0 metaprl/refiner/term_std/term_std_sig.ml