diff options
| author | Pierre-Marie Pédrot | 2015-12-18 12:06:24 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-18 12:26:27 +0100 |
| commit | eee16239f6b00400c8a13b787c310bcb11c37afe (patch) | |
| tree | b1974b3f1b4a3d2ea8f8441d95789049326762d2 /printing/ppvernac.ml | |
| parent | d83e8aceaca972f8997f208e46d257e69c2e352d (diff) | |
Tying the loop in tactic printing API.
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 72b9cafe3f..d79fb45618 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -79,13 +79,7 @@ module Make | VernacEndSubproof -> str"" | _ -> str"." - let pr_gen t = - pr_raw_generic - pr_constr_expr - pr_lconstr_expr - pr_raw_tactic_level - pr_constr_expr - pr_reference t + let pr_gen t = pr_raw_generic (Global.env ()) t let sep = fun _ -> spc() let sep_v2 = fun _ -> str"," ++ spc() |