diff options
| author | ckeller <ckeller@users.noreply.github.com> | 2019-03-11 20:25:35 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-11 20:25:35 +0100 |
| commit | a88e3b3b6ad01a9b85c828b9a1225732275affee (patch) | |
| tree | acc3768695698a80867b4ce941ab4cb7b4b99d7a /src/smtlib2/smtlib2_genConstr.ml | |
| parent | 33010bfa6345549d8b9b0c06f44150b60d0c86e5 (diff) | |
| download | smtcoq-a88e3b3b6ad01a9b85c828b9a1225732275affee.tar.gz smtcoq-a88e3b3b6ad01a9b85c828b9a1225732275affee.zip | |
V8.8 (#42)
* Towards 8.8
* Towards 8.8
* Towards 8.8
* Towards 8.8
* Towards 8.8
* Towards 8.8
* Towards 8.8
* Organization structures
* 8.8 ok with standard coq
Diffstat (limited to 'src/smtlib2/smtlib2_genConstr.ml')
| -rw-r--r-- | src/smtlib2/smtlib2_genConstr.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml index 203077b..64f0b20 100644 --- a/src/smtlib2/smtlib2_genConstr.ml +++ b/src/smtlib2/smtlib2_genConstr.ml @@ -98,10 +98,10 @@ let rec sort_of_sort = function let declare_sort rt sym = let s = string_of_symbol sym in - let cons_t = declare_new_type (Names.id_of_string ("Smt_sort_"^s)) in + let cons_t = Structures.declare_new_type (Structures.mkId ("Smt_sort_"^s)) in let compdec_type = mklApp cCompDec [| cons_t |] in let compdec_var = - declare_new_variable (Names.id_of_string ("CompDec_"^s)) compdec_type in + Structures.declare_new_variable (Structures.mkId ("CompDec_"^s)) compdec_type in let ce = mklApp cTyp_compdec [|cons_t; compdec_var|] in let res = SmtBtype.declare rt cons_t ce in VeritSyntax.add_btype s res; @@ -115,7 +115,7 @@ let declare_fun rt ro sym arg cod = let coqTy = List.fold_right (fun typ c -> Term.mkArrow (interp_to_coq rt typ) c) tyl (interp_to_coq rt ty) in - let cons_v = declare_new_variable (Names.id_of_string ("Smt_var_"^s)) coqTy 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 VeritSyntax.add_fun s op; op |