diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-11 20:01:04 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-11 20:01:04 +0000 |
| commit | 0601db38b579513e4ab39a161591cd359260490e (patch) | |
| tree | 2741c3b805ec8b890c5b9f58aeb1445ec10590fc /proofs | |
| parent | 8556f4e4b5e21535013e6962feabfede6313462b (diff) | |
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
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 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)) |