diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-26 11:23:53 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-26 11:23:53 +0200 |
| commit | 660364faca9dc1708b746c50aac9de6262de1d96 (patch) | |
| tree | 1ff88a54ff9bf847b5a512dd4c2908858423537f /src/lia | |
| parent | bce2346a26f87e6fed7376d9d8c9050504d048ea (diff) | |
| download | smtcoq-660364faca9dc1708b746c50aac9de6262de1d96.tar.gz smtcoq-660364faca9dc1708b746c50aac9de6262de1d96.zip | |
Port ocaml part
Diffstat (limited to 'src/lia')
| -rw-r--r-- | src/lia/lia.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/lia/lia.ml b/src/lia/lia.ml index dce79ee..6bc205a 100644 --- a/src/lia/lia.ml +++ b/src/lia/lia.ml @@ -167,7 +167,7 @@ let lia_enum = ref true let max_depth = max_int let lia_proof_depth = ref max_depth let get_lia_option () = - (!Structures.Micromega_plugin_Certificate.use_simplex,!lia_enum,!lia_proof_depth) + (Structures.Micromega_plugin_Certificate.use_simplex (),!lia_enum,!lia_proof_depth) let lift_pexpr_prover p l = p (List.map (fun (e,o) -> Structures.Micromega_plugin_Micromega.denorm e , o) l) @@ -249,7 +249,7 @@ let pp_nat o n = Printf.fprintf o "%i" (Structures.Micromega_plugin_Mutils.CoqTo let pp_positive o x = Printf.fprintf o "%i" (Structures.Micromega_plugin_Mutils.CoqToCaml.positive x) -let pp_z o x = Printf.fprintf o "%s" (Big_int.string_of_big_int (Structures.Micromega_plugin_Mutils.CoqToCaml.z_big_int x)) +let pp_z o x = Printf.fprintf o "%s" (Structures.Micromega_plugin_NumCompat.Z.to_string (Structures.Micromega_plugin_Mutils.CoqToCaml.z_big_int x)) let pp_list op cl elt o l = let rec _pp o l = |