From dd98363034c871ac858257cf71f089ca03c17ac1 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 17 Sep 2014 14:20:05 +0200 Subject: Don't raise an error when printing intro-patterns in [functional induction]. --- plugins/funind/g_indfun.ml4 | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index a597e5d454..6e46d36253 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"" | None -> mt () -*) let out_disjunctive = function | loc, IntroAction (IntroOrAndPattern l) -> (loc,l) -- cgit v1.2.3