diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/top_printers.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index cf73540e5f..fa92245239 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -98,7 +98,9 @@ let print_uni u = (pp (pr_uni u)) let pp_universes u = pp (str"[" ++ pr_universes u ++ str"]") -let ppenv e = pp (pr_rel_context e (rel_context e)) +let ppenv e = pp + (str "[" ++ pr_named_context_of e ++ str "]" ++ spc() ++ + str "[" ++ pr_rel_context e (rel_context e) ++ str "]") let pptac = (fun x -> pp(Pptactic.pr_glob_tactic x)) |