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 /tactics | |
| parent | d83e8aceaca972f8997f208e46d257e69c2e352d (diff) | |
Tying the loop in tactic printing API.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 6ac16bd76a..3295b932b9 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -60,9 +60,7 @@ let push_appl appl args = | UnnamedAppl -> UnnamedAppl | GlbAppl l -> GlbAppl (List.map (fun (h,vs) -> (h,vs@args)) l) let pr_generic arg = - let pr_gtac _ x = Pptactic.pr_glob_tactic (Global.env()) x in - try - Pptactic.pr_top_generic pr_constr pr_lconstr pr_gtac pr_constr_pattern arg + try Pptactic.pr_top_generic (Global.env ()) arg with e when Errors.noncritical e -> str"<generic>" let pr_appl h vs = Pptactic.pr_ltac_constant h ++ spc () ++ |