From b8563a155f095f7127c0bde367552d67ce3d1dd3 Mon Sep 17 00:00:00 2001
From: Andrei Paskevich <andrei@tertium.org>
Date: Sun, 25 Apr 2010 19:15:51 +0000
Subject: [PATCH] do not export f_map_pos and f_map_neg: traversal functions
 like f_map_sign should only be applied from specialized recursive functions
 and these funcitons will usually supply the polarity argument.

---
 src/core/term.ml              | 3 ---
 src/core/term.mli             | 3 ---
 src/transform/eliminate_if.ml | 4 ++--
 3 files changed, 2 insertions(+), 8 deletions(-)

diff --git a/src/core/term.ml b/src/core/term.ml
index 2b58dbfeb..dd8dedbc9 100644
--- a/src/core/term.ml
+++ b/src/core/term.ml
@@ -975,9 +975,6 @@ let f_map_sign fnT fnF sign f = f_label_copy f (match f.f_node with
         else f_or (f_and f1p f2) (f_and (f_not f1n) f3)
   | _ -> f_map fnT (fnF sign) f)
 
-let f_map_pos fnT fnF f = f_map_sign fnT fnF true f
-let f_map_neg fnT fnF f = f_map_sign fnT fnF false f
-
 (* safe opening fold *)
 
 let t_branch fn acc b = let _,t = t_open_branch b in fn acc t
diff --git a/src/core/term.mli b/src/core/term.mli
index 3fa183644..dbb9f1c35 100644
--- a/src/core/term.mli
+++ b/src/core/term.mli
@@ -284,9 +284,6 @@ val f_map_sign : (term -> term) -> (bool -> fmla -> fmla) ->
 
     nb: if-then-else and iff are translated if needed *)
 
-val f_map_pos : (term -> term) -> (bool -> fmla -> fmla) -> fmla -> fmla
-val f_map_neg : (term -> term) -> (bool -> fmla -> fmla) -> fmla -> fmla
-
 val t_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> term -> 'a
 val f_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> fmla -> 'a
 
diff --git a/src/transform/eliminate_if.ml b/src/transform/eliminate_if.ml
index 33b721737..81c16a8fa 100644
--- a/src/transform/eliminate_if.ml
+++ b/src/transform/eliminate_if.ml
@@ -73,7 +73,7 @@ let add_ld axl d = match d with
             axl, make_ls_defn ls vl (e_map elim_t elim_f e)
       end
 
-let remove_if_decl d = match d.d_node with
+let elim d = match d.d_node with
   | Dlogic l ->
       let axl, l = map_fold_left add_ld [] l in
       let d = create_logic_decl l in
@@ -82,7 +82,7 @@ let remove_if_decl d = match d.d_node with
       [decl_map (fun _ -> assert false) elim_f d]
 
 let eliminate_if_term =
-  Register.store (fun () -> Trans.decl remove_if_decl None)
+  Register.store (fun () -> Trans.decl elim None)
 
 let () = Register.register_transform "eliminate_if_term" eliminate_if_term
 
-- 
GitLab