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 +-
 plugins/funind/indfun.mli   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 1d63fe01a9..e688204a44 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
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index f88a72ff51..34985f2c48 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -10,7 +10,7 @@ val functional_induction :
   bool ->
   Term.constr ->
   (Term.constr * Term.constr bindings) option ->
-  or_and_intro_pattern_expr Loc.located option ->
+  Term.constr or_and_intro_pattern_expr Loc.located option ->
   Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma
 
 
-- 
cgit v1.2.3