diff options
Diffstat (limited to 'src/trace')
-rw-r--r-- | src/trace/coqInterface.ml | 4 | ||||
-rw-r--r-- | src/trace/coqInterface.mli | 3 | ||||
-rw-r--r-- | src/trace/smtCommands.ml | 2 |
3 files changed, 3 insertions, 6 deletions
diff --git a/src/trace/coqInterface.ml b/src/trace/coqInterface.ml index a8af566..f33f091 100644 --- a/src/trace/coqInterface.ml +++ b/src/trace/coqInterface.ml @@ -152,8 +152,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 @@ -164,7 +162,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/trace/coqInterface.mli b/src/trace/coqInterface.mli index 86fdd95..af34d87 100644 --- a/src/trace/coqInterface.mli +++ b/src/trace/coqInterface.mli @@ -99,10 +99,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 diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index 2108da4..27ba80c 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -681,7 +681,7 @@ let gen_rel_name = let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma = let warn () = - CoqInterface.warning "Lemma" ("Discarding the following lemma (unsupported): "^(Pp.string_of_ppcmds (Ppconstr.pr_constr_expr Environ.empty_env Evd.empty (CoqInterface.extern_constr clemma)))); + CoqInterface.warning "Lemma" ("Discarding the following lemma (unsupported): "^(SmtMisc.string_coq_constr clemma)); None in |