diff options
Diffstat (limited to 'src/trace/smtCommands.ml')
| -rw-r--r-- | src/trace/smtCommands.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index 080d6c6..f626a96 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -115,7 +115,7 @@ let interp_conseq_uf t_i (prem, concl) = let tf = Hashtbl.create 17 in let rec interp = function | [] -> mklApp cis_true [|interp_uf t_i ta tf concl|] - | c::prem -> Term.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in + | c::prem -> Structures.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in interp prem @@ -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 (Structures.extern_constr clemma)))); + 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)))); None in |