aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtBtype.mli
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@inria.fr>2019-01-29 14:51:31 +0100
committerChantal Keller <Chantal.Keller@inria.fr>2019-01-29 14:51:31 +0100
commit3165bb9c1853cd2e471e28c52418dee865d181c3 (patch)
tree35bd4edf8afe2b1d6773e435b07b887ca509338c /src/trace/smtBtype.mli
parent7021c53d4ecf97c82ccebb6bb45f5305d8b482ea (diff)
downloadsmtcoq-3165bb9c1853cd2e471e28c52418dee865d181c3.tar.gz
smtcoq-3165bb9c1853cd2e471e28c52418dee865d181c3.zip
Cleanup
Diffstat (limited to 'src/trace/smtBtype.mli')
-rw-r--r--src/trace/smtBtype.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/trace/smtBtype.mli b/src/trace/smtBtype.mli
index 559e809..4f8d4ad 100644
--- a/src/trace/smtBtype.mli
+++ b/src/trace/smtBtype.mli
@@ -59,6 +59,6 @@ val interp : Term.constr -> btype -> Term.constr
val interp_to_coq : reify_tbl -> btype -> Term.constr
-val get_cuts : reify_tbl -> (Structures.names_id_t * Term.types) list
+val get_cuts : reify_tbl -> (Structures.names_id * Term.types) list
val logic : btype -> logic