aboutsummaryrefslogtreecommitdiffstats
path: root/src/smtlib2
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@inria.fr>2020-03-31 20:25:05 +0200
committerChantal Keller <Chantal.Keller@inria.fr>2020-03-31 20:25:05 +0200
commit20831b39a73ebd38336f19ad4ddb4d6b1078d60d (patch)
tree9e4ec27753feff8f7e95274f99eaa977b546c030 /src/smtlib2
parent4c8654c57666e27637ba2f60ee5c6455176c7a1d (diff)
downloadsmtcoq-20831b39a73ebd38336f19ad4ddb4d6b1078d60d.tar.gz
smtcoq-20831b39a73ebd38336f19ad4ddb4d6b1078d60d.zip
Compiles with Coq-8.10
Diffstat (limited to 'src/smtlib2')
-rw-r--r--src/smtlib2/smtlib2_genConstr.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml
index f938671..7e58aa3 100644
--- a/src/smtlib2/smtlib2_genConstr.ml
+++ b/src/smtlib2/smtlib2_genConstr.ml
@@ -111,7 +111,7 @@ let declare_sort rt sym = declare_sort_from_name rt (string_of_symbol sym)
let declare_fun_from_name rt ro s tyl ty =
let coqTy = List.fold_right (fun typ c ->
- Term.mkArrow (interp_to_coq rt typ) c)
+ Structures.mkArrow (interp_to_coq rt typ) c)
tyl (interp_to_coq rt ty) in
let cons_v = Structures.declare_new_variable (Structures.mkId ("Smt_var_"^s)) coqTy in
let op = Op.declare ro cons_v (Array.of_list tyl) ty None in