From 72498d6d68ac12ba4db0db7d54f0ac6fdaaf0c61 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 18 Aug 2014 17:13:19 +0200 Subject: Adding a new intro-pattern for "apply in" on the fly. Using syntax "pat/term" for "apply term on current_hyp as pat". --- plugins/funind/g_indfun.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind/g_indfun.ml4') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 1d63fe01a..e688204a4 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -80,7 +80,7 @@ END let pr_intro_as_pat prc _ _ pat = match pat with | Some pat -> - spc () ++ str "as" ++ spc () ++ Miscprint.pr_intro_pattern pat + spc () ++ str "as" ++ spc () ++ Miscprint.pr_intro_pattern prc pat | None -> mt () let out_disjunctive = function -- cgit v1.2.3