diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/evar_refiner.mli | 2 | ||||
| -rw-r--r-- | proofs/refiner.ml | 2 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 4 |
3 files changed, 4 insertions, 4 deletions
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index ab0fdf8314..0bd6168095 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -21,7 +21,7 @@ open Rawterm (* Refinement of existential variables. *) val w_refine : evar * evar_info -> - (var_map * unbound_ltac_var_map) * rawconstr -> evar_defs -> evar_defs + (var_map * unbound_ltac_var_map) * rawconstr -> evar_map -> evar_map val instantiate_pf_com : int -> Topconstr.constr_expr -> pftreestate -> pftreestate diff --git a/proofs/refiner.ml b/proofs/refiner.ml index c66e9c84bb..c9c956a1ce 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -939,4 +939,4 @@ let print_pftreestate {tpf = pf; tpfsigma = sigma; tstack = stack } = prlist_with_sep (fun () -> str ";") (fun (n,_) -> int n) (List.rev stack) ++ str "] is:")) ++ fnl() ++ !pp_proof sigma (Global.named_context()) pf ++ - Evd.pr_evar_defs sigma + Evd.pr_evar_map sigma diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index acccfb812d..9e35abfc89 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -244,9 +244,9 @@ let rec pr_list f = function | a::l1 -> (f a) ++ pr_list f l1 let pr_gls gls = - hov 0 (pr_evar_defs (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) + hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) let pr_glls glls = - hov 0 (pr_evar_defs (sig_sig glls) ++ fnl () ++ + hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++ prlist_with_sep pr_fnl db_pr_goal (sig_it glls)) |