From c2bde259c207f9ff9cb199906879cd1e19a75ced Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 23 Aug 2014 18:15:16 +0200
Subject: Tactics.is_quantified_hypothesis does not reduce anymore to decide
 whether a variable is quantified in the goal. This is only used by induction,
 and it should be a bad practice to depend on an invisible binder.

---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5c76ce776b..83e282a303 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -677,7 +677,7 @@ let pf_lookup_hypothesis_as_renamed_gen red h gl =
   with Redelimination -> None
 
 let is_quantified_hypothesis id g =
-  match pf_lookup_hypothesis_as_renamed_gen true (NamedHyp id) g with
+  match pf_lookup_hypothesis_as_renamed_gen false (NamedHyp id) g with
     | Some _ -> true
     | None -> false
 
-- 
cgit v1.2.3