From 841bc4617470a30d4025fc279c5a3e72edbb6e13 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 31 Oct 2010 21:19:29 +0000
Subject: An experimental support for open constrs in hints and in "using"
 option of "auto". Works for not too complicated hints (e.g. "@pair _ _ 0").
 Would be simpler if make_apply_entry supported lemmas containing evars.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13598 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/functional_principles_proofs.ml | 2 +-
 plugins/funind/recdef.ml                       | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 43658e8021..e047f13d53 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1450,7 +1450,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 				    Eauto.eauto_with_bases
 				      false
 				      (true,5)
-				      [Lazy.force refl_equal]
+				      [Evd.empty,Lazy.force refl_equal]
 				      [Auto.Hint_db.empty empty_transparent_state false]
 				  )
 			   )
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 057ffb9b32..f066e39d05 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1005,7 +1005,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 		      Eauto.eauto_with_bases
 			false
 			(true,5)
-			[delayed_force refl_equal]
+			[Evd.empty,delayed_force refl_equal]
 			[Auto.Hint_db.empty empty_transparent_state false]
 		      ]
 		    )
-- 
cgit v1.2.3