diff options
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index fccee6e40..6f4ef37b4 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -574,9 +574,7 @@ module Make str "=>" ++ brk (1,4) ++ pr t)) | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t - let pr_funvar = function - | None -> spc () ++ str "_" - | Some id -> spc () ++ pr_id id + let pr_funvar n = spc () ++ pr_name n let pr_let_clause k pr (id,(bl,t)) = hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++ |