diff options
Diffstat (limited to 'src/versions/standard/structures.ml')
-rw-r--r-- | src/versions/standard/structures.ml | 5 |
1 files changed, 2 insertions, 3 deletions
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, _, _) -> |