aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtBtype.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/trace/smtBtype.ml')
-rw-r--r--src/trace/smtBtype.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml
index 0ebb893..119c046 100644
--- a/src/trace/smtBtype.ml
+++ b/src/trace/smtBtype.ml
@@ -119,8 +119,8 @@ let to_list reify =
let make_t_i rt = interp_tbl rt
-let interp_t t_i t =
- mklApp cinterp_t [|t_i ; to_coq t|]
+(* let interp_t t_i t =
+ * mklApp cinterp_t [|t_i ; to_coq t|] *)
let dec_interp t_i t =
mklApp cdec_interp [|t_i ; to_coq t|]