From 2c26c287cc36dcbecb4b41ca3a7a3f58bff07ac2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Nov 2014 19:55:59 +0100
Subject: Fixing 1177da327 (reorganization of the test for generic selection of
 occurrences: some uniformisation was not appropriate for "change").

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

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4d8c97870d..23ec74db0f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3877,7 +3877,7 @@ let pose_induction_arg clear_flag isrec with_evars info_arg elim
 end
 
 let has_generic_occurrences_but_goal cls id env ccl =
-  clause_with_generic_occurrences cls &&
+  clause_with_generic_context_selection cls &&
   (* TODO: whd_evar of goal *)
   (cls.concl_occs != NoOccurrences || not (occur_var env id ccl))
 
-- 
cgit v1.2.3