diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-17 14:20:05 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-11-01 22:43:57 +0100 |
| commit | dd98363034c871ac858257cf71f089ca03c17ac1 (patch) | |
| tree | a7e71827aaa4a3815073e1c49723ff19798fa6ec /plugins/funind/g_indfun.ml4 | |
| parent | 53c3b382b4ca82e4589d2f5e574df688ab7957de (diff) | |
Don't raise an error when printing intro-patterns in [functional induction].
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) |