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/indfun.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind/indfun.mli')

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