More modularity on the format of traces depending on the version of coq

1 files changed, 24 insertions, 24 deletions

diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index b3248ef..74d3170 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -352,31 +352,31 @@ let to_coq to_lit interp (cstep,
   let nc = ref 0 in
   while not (isRoot !r.kind) do r := prev !r; incr nc done;
   let last_root = !r in
-  let size = !nc in
-  let max = Structures.max_array_size - 1 in
-  let q,r1 = size / max, size mod max in
-
-  let trace = 
-    let len = if r1 = 0 then q + 1 else q + 2 in
-    Array.make len (Structures.mkArray (step, [|def_step|])) in
-  for j = 0 to q - 1 do
-    let tracej = Array.make Structures.max_array_size def_step in
-    for i = 0 to max - 1 do
-      r := next !r;
-      tracej.(i) <- step_to_coq !r; 
-    done;
-    trace.(j) <- Structures.mkArray (step, tracej)
-  done;
-  if r1 <> 0 then begin
-    let traceq = Array.make (r1 + 1) def_step in
-    for i = 0 to r1-1 do 
-    r := next !r; 
-    traceq.(i) <- step_to_coq !r; 
-    done;
-    trace.(q) <- Structures.mkArray (step, traceq)
-  end;
 
-  (Structures.mkArray (mklApp carray [|step|], trace), last_root, !cuts)
+  (* let size = !nc in *)
+  (* let max = Structures.max_array_size - 1 in *)
+  (* let q,r1 = size / max, size mod max in *)
+  (* let trace =  *)
+  (*   let len = if r1 = 0 then q + 1 else q + 2 in *)
+  (*   Array.make len (Structures.mkArray (step, [|def_step|])) in *)
+  (* for j = 0 to q - 1 do *)
+  (*   let tracej = Array.make Structures.max_array_size def_step in *)
+  (*   for i = 0 to max - 1 do *)
+  (*     r := next !r; *)
+  (*     tracej.(i) <- step_to_coq !r;  *)
+  (*   done; *)
+  (*   trace.(j) <- Structures.mkArray (step, tracej) *)
+  (* done; *)
+  (* if r1 <> 0 then begin *)
+  (*   let traceq = Array.make (r1 + 1) def_step in *)
+  (*   for i = 0 to r1-1 do  *)
+  (*   r := next !r;  *)
+  (*   traceq.(i) <- step_to_coq !r;  *)
+  (*   done; *)
+  (*   trace.(q) <- Structures.mkArray (step, traceq) *)
+  (* end; *)
+  (* (Structures.mkArray (mklApp carray [|step|], trace), last_root, !cuts) *)
+  (Structures.mkTrace step_to_coq next carray clist cnil ccons cpair !nc step def_step r, last_root, !cuts)