diff options
Diffstat (limited to 'plugins/funind/g_indfun.ml4')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index a597e5d45..6e46d3625 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -77,14 +77,12 @@ TACTIC EXTEND newfuninv END -let pr_intro_as_pat prc _ _ pat = - failwith "todo" -(* +let pr_intro_as_pat _prc _ _ pat = match pat with | Some pat -> - spc () ++ str "as" ++ spc () ++ Miscprint.pr_intro_pattern prc pat + spc () ++ str "as" ++ spc () ++ (* Miscprint.pr_intro_pattern prc pat *) + str"<simple_intropattern>" | None -> mt () -*) let out_disjunctive = function | loc, IntroAction (IntroOrAndPattern l) -> (loc,l) |