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 /plugins/subtac/subtac_utils.ml | |
| 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 'plugins/subtac/subtac_utils.ml')
| -rw-r--r-- | plugins/subtac/subtac_utils.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml index 64f5fe9c7..0beb1e1ae 100644 --- a/plugins/subtac/subtac_utils.ml +++ b/plugins/subtac/subtac_utils.ml @@ -116,7 +116,7 @@ let my_print_context = Termops.print_rel_context let my_print_named_context = Termops.print_named_context let my_print_env = Termops.print_env let my_print_rawconstr = Printer.pr_rawconstr_env -let my_print_evardefs = Evd.pr_evar_defs +let my_print_evardefs = Evd.pr_evar_map let my_print_tycon_type = Evarutil.pr_tycon_type @@ -448,7 +448,7 @@ let pr_evar_info evi = in hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]") -let pr_evar_defs sigma = +let pr_evar_map sigma = h 0 (prlist_with_sep pr_fnl (fun (ev,evi) -> @@ -464,11 +464,11 @@ let pr_constraints pbs = | Reduction.CUMUL -> "<=") ++ spc() ++ print_constr t2) pbs) -let pr_evar_defs evd = +let pr_evar_map evd = let pp_evm = let evars = evd in if evars = empty then mt() else - str"EVARS:"++brk(0,1)++pr_evar_defs evars++fnl() in + str"EVARS:"++brk(0,1)++pr_evar_map evars++fnl() in let pp_met = if meta_list evd = [] then mt() else str"METAS:"++brk(0,1)++pr_meta_map evd in |