From 0601db38b579513e4ab39a161591cd359260490e Mon Sep 17 00:00:00 2001 From: glondu Date: Wed, 11 Nov 2009 20:01:04 +0000 Subject: Promote evar_defs to evar_map (in Evd) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12502 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/evar_refiner.mli | 2 +- proofs/refiner.ml | 2 +- proofs/tacmach.ml | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) (limited to 'proofs') diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index ab0fdf831..0bd616809 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 c66e9c84b..c9c956a1c 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 acccfb812..9e35abfc8 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)) -- cgit v1.2.3