Some clean up

src/ecLowGoal.ml

@@ -1512,9 +1512,6 @@ let t_elim_iso_or ?reduce tc =
 
 (* -------------------------------------------------------------------- *)
 let t_split_and_i i b f1 f2 tc =
-  (* if i <= 0 then *)
-  (*   t_and_intro_s b (f1, f2) tc *)
-  (* else *)
   let i = i - 1 in
   let rec destr acc_sym acc_f i f =
     if i < 0 then
@@ -1525,22 +1522,23 @@ let t_split_and_i i b f1 f2 tc =
         destr (b :: acc_sym) (f1 :: acc_f) (i - 1) f2
       | _ -> tc_error !!tc ~catchable:true  "not enought conjunctions" in
 
-  let rec constr l_sym l_f =
-    match l_sym, l_f with
-    | [_], [f] -> f
-    | `Asym :: sym , f :: fs -> f_anda f (constr sym fs)
-    | `Sym :: sym,  f :: fs -> f_and f (constr sym fs)
-    | _, _ -> assert false in
+  let l_sym , l_fsl, fsr = destr [b] [f1] i f2 in
 
-  let l_sym , l_f, fsr = destr [b] [f1] i f2 in
-  let fsl = constr (List.rev l_sym) (List.rev l_f) in
+  let sym = List.hd l_sym in
+  let syms = List.tl l_sym in
+  let fsl = List.hd l_fsl in
+  let fsls = List.tl l_fsl in
+
+  let fsl =
+    List.fold_left2(fun acc sym f ->
+      match sym with
+      | `Asym -> f_anda f acc
+      | `Sym  -> f_and f acc
+    ) fsl syms fsls in
 
   let tc = FApi.tcenv_of_tcenv1 tc in
   let tc, gl = FApi.newgoal tc fsl in
 
-  let sym = List.hd l_sym in
-  let syms = List.rev (List.tl l_sym) in
-
   let tc, gr =
     match sym with
     | `Asym ->
@@ -1549,8 +1547,7 @@ let t_split_and_i i b f1 f2 tc =
       tc,`App (`HD gr, [`Sub (`HD gl:>prept)])
     | `Sym ->
       let tc, gr = FApi.newgoal tc fsr in
-      tc,(`HD gr:>prept)
-  in
+      tc,(`HD gr:>prept) in
 
   let pelim (sym : [`Sym | `Asym]) (side : [`L | `R]) =
     match sym, side with
@@ -1568,7 +1565,7 @@ let t_split_and_i i b f1 f2 tc =
         let j = pt_of_prept_r pte j in
         let h = pt_of_prept_r pte h in
         (`PE h, (sym, `PE j))
-      ) (`HD gl :> prept) syms in
+      ) (`HD gl :> prept) (List.rev syms) in
 
   let projs = projs @ [sym, proj] in