1 files changed, 15 insertions, 0 deletions
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index 6921593..bf53f41 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -43,6 +43,7 @@ let mkInt : int -> Term.constr = fun i ->
 
 let cint = gen_constant int31_module "int31"
 
+
 (* PArray *)
 let parray_modules = [["SMTCoq";"versions";"standard";"Array";"PArray"]]
 
@@ -63,6 +64,20 @@ let mkArray : Term.types * Term.constr array -> Term.constr =
                        ) (0,mklApp cmake [|ty; mkInt l; a.(l)|]) a)
 
 
+(* Traces *)
+(* WARNING: side effect on r! *)
+let mkTrace step_to_coq next _ clist cnil ccons cpair size step def_step r =
+  let rec mkTrace s =
+    if s = size then
+      mklApp cnil [|step|]
+    else (
+      r := next !r;
+      let st = step_to_coq !r in
+      mklApp ccons [|step; st; mkTrace (s+1)|]
+    ) in
+  mklApp cpair [|mklApp clist [|step|]; step; mkTrace 0; def_step|]
+
+
 (* Differences between the two versions of Coq *)
 type names_id_t = Names.Id.t