From 9ab628374131e60217d550d670027b531125a74e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 26 Sep 2011 11:47:26 +0000
Subject: Added support for referring to subterms of the goal by pattern.
 Tactics set/remember and destruct/induction take benefit of it.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14499 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/indfun.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 85c362b769..1ce6564c1c 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -75,7 +75,7 @@ let functional_induction with_clean c princl pat =
 	if princ_infos.Tactics.farg_in_concl
 	then [c] else []
       in
-      List.map (fun c -> Tacexpr.ElimOnConstr (c,NoBindings)) (args@c_list)
+      List.map (fun c -> Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))) (args@c_list)
     in
     let princ' = Some (princ,bindings) in
     let princ_vars =
-- 
cgit v1.2.3