split does not introduce extras disjunctions

src/core/term.ml

@@ -1242,7 +1242,7 @@ let f_map_sign fnT fnF sign f = f_label_copy f (match f.f_node with
       let f1p = fnF sign f1 in let f1n = fnF (not sign) f1 in
       let f2 = fnF sign f2 in let f3 = fnF sign f3 in
       if f_equal f1p f1n then f_if f1p f2 f3 else if sign
-        then f_and (f_implies f1n f2) (f_or f1p f3)
+        then f_and (f_implies f1n f2) (f_implies (f_not f1p) f3)
         else f_or (f_and f1p f2) (f_and (f_not f1n) f3)
   | _ -> f_map fnT (fnF sign) f)
 

src/ide/db.ml

@@ -1064,23 +1064,23 @@ let root_goals () =
 *)
 
 
-let add_file = assert false
-let add_theory = assert false
-let add_goal = assert false
-let add_transformation = assert false
-let set_edited_as = assert false
-let set_obsolete = assert false
-let set_status = assert false
-let add_proof_attempt = assert false
-let prover_from_name = assert false
+let add_file _ = assert false
+let add_theory _ = assert false
+let add_goal _ = assert false
+let add_transformation _ = assert false
+let set_edited_as _ = assert false
+let set_obsolete _ = assert false
+let set_status _ = assert false
+let add_proof_attempt _ = assert false
+let prover_from_name _ = assert false
 exception AlreadyExist 
-let files = assert false
-let init_base = assert false
-let theories = assert false
-let file_name = assert false
-let verified = assert false
-let goals = assert false
-let theory_name = assert false
+let files _ = assert false
+let init_base _ = assert false
+let theories _ = assert false
+let file_name _ = assert false
+let verified _ = assert false
+let goals _ = assert false
+let theory_name _ = assert false
 
 
 (*

src/transform/eliminate_if.ml

@@ -95,7 +95,7 @@ and elim_f sign f = match f.f_node with
       let f1n = elim_f (not sign) f1 in
       let f2 = elim_f sign f2 in
       let f3 = elim_f sign f3 in
-      if sign then f_and (f_implies f1n f2) (f_or f1p f3)
+      if sign then f_and (f_implies f1n f2) (f_implies (f_not f1p) f3)
               else f_or (f_and f1p f2) (f_and (f_not f1n) f3)
   | _ ->
       f_map_sign elim_t elim_f sign f

src/transform/split_goal.ml

@@ -56,7 +56,8 @@ let rec split_pos acc f = match f.f_node with
   | Fnot f ->
       apply_append f_not acc (split_neg [] f)
   | Fif (fif,fthen,felse) ->
-      split_pos (split_pos acc (f_implies fif fthen)) (f_or fif felse)
+      split_pos (split_pos acc (f_implies fif fthen)) 
+        (f_implies (f_not fif) felse)
   | Flet (t,fb) -> let vs,f = f_open_bound fb in
       apply_append (f_let_close vs t) acc (split_pos [] f)
   | Fcase (tl,bl) ->

src/transform/split_goal.mli

@@ -20,7 +20,12 @@
 val asym_split : Ident.label
 
 val split_pos : Term.fmla list -> Term.fmla -> Term.fmla list
+(** [split_pos l f] returns a list [g1;..;gk] @ l such that
+ f is logically equivalent to g1 /\ .. /\ gk *)
+
 val split_neg : Term.fmla list -> Term.fmla -> Term.fmla list
+(** [split_neg l f] returns a list [g1;..;gk] @ l such that
+ f is logically equivalent to g1 \/ .. \/ gk *)
 
 val split_goal : Task.task Trans.tlist
 val split_all  : Task.task Trans.tlist