diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index ca90b37593..cc9ae912dc 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -78,7 +78,8 @@ END let pr_intro_as_pat prc _ _ pat = match pat with - | Some pat -> spc () ++ str "as" ++ spc () ++ pr_intro_pattern pat + | Some pat -> + spc () ++ str "as" ++ spc () ++ Miscprint.pr_intro_pattern pat | None -> mt () |