From 20831b39a73ebd38336f19ad4ddb4d6b1078d60d Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Tue, 31 Mar 2020 20:25:05 +0200 Subject: Compiles with Coq-8.10 --- src/smtlib2/smtlib2_genConstr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/smtlib2/smtlib2_genConstr.ml') 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 -- cgit