3 files changed, 29 insertions, 2 deletions
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index a6d0023..ca5f3cc 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -355,7 +355,6 @@ let rec mk_bv_list = function
 
 
 (* Reification *)
-
 let mk_bool b =
   let c, args = Structures.decompose_app b in
   if Structures.eq_constr c (Lazy.force ctrue) then true
@@ -435,3 +434,27 @@ let mk_bvsize n =
       else assert false
     | _ -> assert false
   else mk_N n
+
+(** Switches between constr and OCaml *)
+(* Transform a option constr into a constr option *)
+let option_of_constr_option co =
+  let c, args = Structures.decompose_app co in
+  if c = Lazy.force cSome then
+    match args with
+      | [_;c] -> Some c
+      | _ -> assert false
+  else
+    None
+
+(* Transform a tuple of constr into a (reversed) list of constr *)
+let list_of_constr_tuple =
+  let rec list_of_constr_tuple acc t =
+    let c, args = Structures.decompose_app t in
+    if c = Lazy.force cpair then
+      match args with
+        | [_;_;t;l] -> list_of_constr_tuple (l::acc) t
+        | _ -> assert false
+    else
+      t::acc
+  in
+  list_of_constr_tuple []
diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli
index bf626b3..b5ca6b7 100644
--- a/src/trace/coqTerms.mli
+++ b/src/trace/coqTerms.mli
@@ -261,3 +261,7 @@ val mk_nat : Structures.constr -> int
 val mk_N : Structures.constr -> int
 val mk_Z : Structures.constr -> int
 val mk_bvsize : Structures.constr -> int
+
+(* Switches between constr and OCaml *)
+val option_of_constr_option : Structures.constr -> Structures.constr option
+val list_of_constr_tuple : Structures.constr -> Structures.constr list
diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
index 92f0f09..aad8b07 100644
--- a/src/trace/smtMisc.ml
+++ b/src/trace/smtMisc.ml
@@ -23,8 +23,8 @@ let mkInt i =
 (** Generic representation of shared object *)
 type 'a gen_hashed = { index : int; hval : 'a }
 
-(** Functions over constr *)
 
+(** Functions over constr *)
 let mklApp f args = Structures.mkApp (Lazy.force f, args)
 
 let string_of_name_def d n = try Structures.string_of_name n with | _ -> d