diff options
Diffstat (limited to 'ltac/tacentries.ml')
| -rw-r--r-- | ltac/tacentries.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 2e2b55be7..75edf150e 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -504,10 +504,7 @@ let print_ltacs () = | Tacexpr.TacFun (l, t) -> (l, t) | _ -> ([], body) in - let pr_ltac_fun_arg = function - | None -> spc () ++ str "_" - | Some id -> spc () ++ pr_id id - in + let pr_ltac_fun_arg n = spc () ++ pr_name n in hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l) in Feedback.msg_notice (prlist_with_sep fnl pr_entry entries) |