From 5dcafa956e49eefc451dd021a0fe8ad2e2338088 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 15 Aug 2014 17:43:35 +0200
Subject: Lazy interpretation of patterns so that expressions such as "intros H
 H'/H" can be given with second H bound by the first one.

Not very satisfied by passing closure to tactics.ml, but otherwise
tactics would have to be aware of glob_constr.
---
 plugins/funind/g_indfun.ml4 | 5 ++++-
 plugins/funind/indfun.mli   | 2 +-
 2 files changed, 5 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index e688204a44..bbb8a96c54 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -78,10 +78,13 @@ END
 
 
 let pr_intro_as_pat prc _ _ pat =
+  failwith "todo"
+(*
   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
     | None -> mt ()
+*)
 
 let out_disjunctive = function
   | loc, IntroAction (IntroOrAndPattern l) -> (loc,l)
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 34985f2c48..e720691406 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 ->
-  Term.constr or_and_intro_pattern_expr Loc.located option ->
+  Tacexpr.or_and_intro_pattern option ->
   Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma
 
 
-- 
cgit v1.2.3