Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-15 17:16:05 -0800 (Tue, 15 Nov 2005)
Revision: 8186
Log message:

      A number of improvements in the .prla merging algorithm.
      
      In particular, it now handles cases where one file has a primitive proof and
      another - a real interactive one. In this case the "merge_prla" program will
      always drop the primitive one and keep the interacrive one.
      

Changes  Path
+114 -18 metaprl/filter/filter/filter_merge_prla.ml