remove hack for <= 1.0.8

Author: LdBeth

Diff for: filter/base/filter_magic.ml

@@ -125,8 +125,6 @@ let term_versions = List.map (pack_version 1 0) [34;33;32;31;30;29;28;27;25;24]
  * Rev 27: changed the stging encoding of option_info
  * Rev 28: added "opaque" qualifier to the "define" statements
  *
- * Term_man_minimal_sig has extra stuff for rev 0-7 file support.
- * Filter_summary has a HACK needed to read rev 0-8 files.
  * Proof_term_boot has a HACK needed to read rev 0-9 files.
  * Ascii_io has another HACK needed to read some rev 0-10 files.
  * Filter_summary has another HACK needed to read some rev 0-11 files.

Diff for: filter/base/filter_summary.ml

@@ -1340,16 +1340,9 @@ struct
 
    (*
     * Parent declaration.
-    * XXX HACK: The "if" is here because parent terms used to have 3 subterms in old files
-    * (ASCII IO format <= 1.0.8)
     *)
    let dest_parent convert t =
-      let path, resources =
-         if is_dep0_dep0_term parent_op t then
-            two_subterms t
-         else
-            let p, _, r = three_subterms t
-            in p, r
+      let path, resources = two_subterms t
       in
          Parent { parent_name = dest_string_param_list path;
                   parent_resources = List.map (dest_resource_sig convert) (dest_xlist resources)
@@ -2040,7 +2033,7 @@ struct
                         implem_error loc (sprintf "Cond_rewrite %s: param list mismatch" name)
                      else if not (List.length args = List.length args' && List.for_all2 alpha_equal args' args) then
                         implem_error loc (sprintf "Cond_rewrite %s: arg lists mismatch" name)
-                     else if not (alpha_equal redex' redex & alpha_equal contractum contractum') then
+                     else if not (alpha_equal redex' redex && alpha_equal contractum contractum') then
                         implem_error loc (sprintf "Cond_rewrite %s: specification mismatch" name)
                      else
                         ()
@@ -2505,7 +2498,7 @@ struct
                             rw_proof = proof;
                             _
                   }, _) ->
-               if not (alpha_equal rw.rw_redex redex & alpha_equal rw.rw_contractum contractum) then
+               if not (alpha_equal rw.rw_redex redex && alpha_equal rw.rw_contractum contractum) then
                   eprintf "Copy_proof: warning: rewrite %s%s%t" rw.rw_name changed_warning eflush;
                { rw with rw_proof = copy_proof rw.rw_proof proof }
           | Some (Rule { rule_proof = proof; _ }, _)
@@ -2529,8 +2522,8 @@ struct
                                 _
                   }, _) ->
                if not (alpha_equal crw.crw_redex redex)
-                  or not (alpha_equal crw.crw_contractum contractum)
-                  or not (Lm_list_util.for_all2 alpha_equal crw.crw_assums assums)
+                  || not (alpha_equal crw.crw_contractum contractum)
+                  || not (Lm_list_util.for_all2 alpha_equal crw.crw_assums assums)
                then
                   eprintf "Copy_proof: warning: cond_rewrite %s%s%t" crw.crw_name changed_warning eflush;
                { crw with crw_proof = copy_proof crw.crw_proof proof }

Diff for: filter/filter/filter_merge_prla.ml

@@ -61,7 +61,7 @@ type pf_kind =
 (*
  * XXX: HACK: nogin: the proper way would be to decode the actual module items and then
  * do a proper filtering and merging. However I do not want to write this at the time as
- * I am hoping that it would become much easiere to do this one the new_io branch is
+ * I am hoping that it would become much easiere to do this once the new_io branch is
  * finished and merged.
  *)
 let summary_opname  = mk_opname "Summary"      nil_opname