aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtBtype.ml
diff options
context:
space:
mode:
authorckeller <ckeller@users.noreply.github.com>2022-02-15 18:27:33 +0100
committerGitHub <noreply@github.com>2022-02-15 18:27:33 +0100
commitc163813243e1b38b7d8c10b49d78a728d747e0e5 (patch)
tree7d2d936fc170ad9215aaac2822aa896957456f71 /src/trace/smtBtype.ml
parent1860a878ad5af74f5e2d2142c35b1e2d7c43aad3 (diff)
downloadsmtcoq-c163813243e1b38b7d8c10b49d78a728d747e0e5.tar.gz
smtcoq-c163813243e1b38b7d8c10b49d78a728d747e0e5.zip
Use the Register mechanism (#104)
Diffstat (limited to 'src/trace/smtBtype.ml')
-rw-r--r--src/trace/smtBtype.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml
index c610129..923874e 100644
--- a/src/trace/smtBtype.ml
+++ b/src/trace/smtBtype.ml
@@ -156,7 +156,7 @@ let interp_tbl reify =
| _ -> Some bt
in
Hashtbl.filter_map_inplace set reify.tbl;
- CoqInterface.mkArray (Lazy.force ctyp_compdec, t)
+ CoqTerms.mkArray (Lazy.force ctyp_compdec, t)
let to_list reify =