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 |