Port ocaml part

4 files changed, 7 insertions, 8 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 =
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index f626a96..23ce54b 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -689,7 +689,7 @@ let gen_rel_name =
 
 let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma =
   let warn () =
-    Structures.warning "Lemma" ("Discarding the following lemma (unsupported): "^(Pp.string_of_ppcmds (Ppconstr.pr_constr_expr Environ.empty_env Evd.empty (Structures.extern_constr clemma))));
+    Structures.warning "Lemma" ("Discarding the following lemma (unsupported): "^(SmtMisc.string_coq_constr clemma));
     None
   in
 
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index d069dde..a872e41 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -163,6 +163,7 @@ module Micromega_plugin_Mutils = Micromega_plugin.Mutils
 module Micromega_plugin_Certificate = Micromega_plugin.Certificate
 module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega
 module Micromega_plugin_Persistent_cache = Micromega_plugin.Persistent_cache
+module Micromega_plugin_NumCompat = Micromega_plugin.NumCompat
 
 let micromega_coq_proofTerm =
   (* Cannot contain evars *)
@@ -201,8 +202,6 @@ type constr_expr = Constrexpr.constr_expr
 let error s = CErrors.user_err (Pp.str s)
 let warning n s = CWarnings.create ~name:n ~category:"SMTCoq plugin" Pp.str s
 
-let extern_constr c = Constrextern.extern_constr true Environ.empty_env Evd.empty (EConstr.of_constr c)
-
 let destruct_rel_decl r = Context.Rel.Declaration.get_name r,
                           Context.Rel.Declaration.get_type r
 
@@ -213,7 +212,7 @@ let ppconstr_lsimpleconstr = Ppconstr.lsimpleconstr
 
 let constrextern_extern_constr c =
   let env = Global.env () in
-  Constrextern.extern_constr false env (Evd.from_env env) (EConstr.of_constr c)
+  Constrextern.extern_constr ~inctx:false env (Evd.from_env env) (EConstr.of_constr c)
 
 let get_rel_dec_name = function
   | Context.Rel.Declaration.LocalAssum (n, _) | Context.Rel.Declaration.LocalDef (n, _, _) ->
diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli
index 78c948c..46f9715 100644
--- a/src/versions/standard/structures.mli
+++ b/src/versions/standard/structures.mli
@@ -94,6 +94,7 @@ module Micromega_plugin_Mutils = Micromega_plugin.Mutils
 module Micromega_plugin_Certificate = Micromega_plugin.Certificate
 module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega
 module Micromega_plugin_Persistent_cache = Micromega_plugin.Persistent_cache
+module Micromega_plugin_NumCompat = Micromega_plugin.NumCompat
 
 val micromega_coq_proofTerm : constr lazy_t
 val micromega_dump_proof_term : Micromega_plugin_Micromega.zArithProof -> constr
@@ -113,10 +114,9 @@ val set_evars_tac : constr -> tactic
 type constr_expr = Constrexpr.constr_expr
 val error : string -> 'a
 val warning : string -> string -> unit
-val extern_constr : constr -> constr_expr
 val destruct_rel_decl : (constr, types) Context.Rel.Declaration.pt -> name * types
 val interp_constr : Environ.env -> Evd.evar_map -> constr_expr -> constr
-val ppconstr_lsimpleconstr : Notation_gram.tolerability
+val ppconstr_lsimpleconstr : Constrexpr.entry_relative_level
 val constrextern_extern_constr : constr -> constr_expr
 val get_rel_dec_name : (constr, types) Context.Rel.Declaration.pt -> name
 val retyping_get_type_of : Environ.env -> Evd.evar_map -> constr -> constr