diff options
Diffstat (limited to 'dev/top_printers.ml')
| -rw-r--r-- | dev/top_printers.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index ba0c54407..f9b402586 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -181,7 +181,7 @@ let ppproofview p = pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) sigma) let ppopenconstr (x : Evd.open_constr) = - let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ envpp pr_constr_env c) + let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ envpp pr_econstr_env c) (* spiwack: deactivated until a replacement is found let pppftreestate p = pp(print_pftreestate p) *) |