From 7940ef63c654be26b41ce20162207f3c67d0b10a Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Sun, 28 Oct 2018 00:30:23 +0200 Subject: New files SmtBtype.ml(i) for module formerly in SmtAtom --- src/smtlib2/smtlib2_genConstr.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src/smtlib2/smtlib2_genConstr.ml') diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml index b320d7a..27ac8d3 100644 --- a/src/smtlib2/smtlib2_genConstr.ml +++ b/src/smtlib2/smtlib2_genConstr.ml @@ -19,6 +19,7 @@ open SmtAtom open SmtForm open SmtMisc open CoqTerms +open SmtBtype (* For debugging *) @@ -79,7 +80,7 @@ let declare_sort rt sym = let eq_refl = Term.mkProd (x,cons_t,Term.mkProd (y,cons_t,mklApp creflect [|mklApp ceq [|cons_t;rx;ry|];mklApp (lazy eq_t) [|rx;ry|]|])) in let eq_refl_v = declare_new_variable (Names.id_of_string ("eq_refl_"^s)) eq_refl in let ce = mklApp cTyp_eqb [|cons_t;eq_t;eq_refl_v|] in - let res = Btype.declare rt cons_t ce in + let res = declare rt cons_t ce in VeritSyntax.add_btype s res; res @@ -89,7 +90,7 @@ let declare_fun rt ro sym arg cod = let tyl = List.map sort_of_sort arg in let ty = sort_of_sort cod in - let coqTy = List.fold_right (fun typ c -> Term.mkArrow (Btype.interp_to_coq rt (fst typ)) c) tyl (Btype.interp_to_coq rt (fst ty)) in + let coqTy = List.fold_right (fun typ c -> Term.mkArrow (interp_to_coq rt (fst typ)) c) tyl (interp_to_coq rt (fst ty)) in let cons_v = declare_new_variable (Names.id_of_string ("Smt_var_"^s)) coqTy in let op = Op.declare ro cons_v (Array.of_list (List.map fst tyl)) (fst ty) in -- cgit