Reorganization of the test for generic selection of occurrences in

clause; extended it so that an induction over "x" is considered
generic when the clause has the form "in H |-" (w/o the conclusion)
and x does not occur in the conclusion.

5 files changed, 22 insertions, 24 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index fb09a3108..a57720755 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -174,23 +174,9 @@ let map_int_or_var f = function
 
 let all_concl_occs_clause = { onhyps=Some[]; concl_occs=AllOccurrences }
 
-let has_no_specified_occs cl =
-  let forall ((occs, _), _) = match occs with
-  | AllOccurrences -> true
-  | _ -> false
-  in
-  let hyps = match cl.onhyps with
-  | None -> true
-  | Some hyps -> List.for_all forall hyps in
-  let concl = match cl.concl_occs with
-  | AllOccurrences | NoOccurrences -> true
-  | _ -> false
-  in
-  hyps && concl
-
 let merge_occurrences loc cl = function
   | None ->
-      if has_no_specified_occs cl then (None, cl)
+      if Locusops.clause_with_generic_occurrences cl then (None, cl)
       else
 	user_err_loc (loc,"",str "Found an \"at\" clause without \"with\" clause.")
   | Some (occs, p) ->
@@ -203,7 +189,7 @@ let merge_occurrences loc cl = function
       | { onhyps = Some [(AllOccurrences, id), l]; concl_occs = NoOccurrences } ->
         { cl with onhyps = Some [(occs, id), l] }
       | _ ->
-        if has_no_specified_occs cl then
+        if Locusops.clause_with_generic_occurrences cl then
           user_err_loc (loc,"",str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.")
         else
           user_err_loc (loc,"",str "Cannot use clause \"at\" twice.")
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 7e825b6c2..cc19f01f8 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -102,7 +102,13 @@ let occurrences_of_goal cls =
 
 let in_every_hyp cls = Option.is_empty cls.onhyps
 
-let has_selected_occurrences cls =
-  cls.concl_occs != AllOccurrences ||
-  not (Option.is_empty cls.onhyps) && List.exists (fun ((occs,_),hl) ->
-    occs != AllOccurrences || hl != InHyp) (Option.get cls.onhyps)
+let clause_with_generic_occurrences cls =
+  let hyps = match cls.onhyps with
+  | None -> true
+  | Some hyps ->
+     List.for_all
+       (function ((AllOccurrences,_),InHyp) -> true | _ -> false) hyps in
+  let concl = match cls.concl_occs with
+  | AllOccurrences | NoOccurrences -> true
+  | _ -> false in
+  hyps && concl
diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli
index c1bf2d9ea..1d7c6b72e 100644
--- a/pretyping/locusops.mli
+++ b/pretyping/locusops.mli
@@ -42,4 +42,4 @@ val occurrences_of_hyp : Id.t -> clause -> (occurrences * hyp_location_flag)
 val occurrences_of_goal : clause -> occurrences
 val in_every_hyp : clause -> bool
 
-val has_selected_occurrences : clause -> bool
+val clause_with_generic_occurrences : 'a clause_expr -> bool
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 3f2963bfe..3f6a4e307 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1468,7 +1468,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
     else
       x
   in
-  let likefirst = not (has_selected_occurrences occs) in
+  let likefirst = clause_with_generic_occurrences occs in
   let mkvarid () = mkVar id in
   let compute_dependency _ (hyp,_,_ as d) (sign,depdecls) =
     match occurrences_of_hyp hyp occs with
@@ -1508,7 +1508,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
     in
     let lastlhyp =
       if List.is_empty depdecls then None else Some (pi1(List.last depdecls)) in
-      (id,sign,depdecls,lastlhyp,ccl,out test)
+    (id,sign,depdecls,lastlhyp,ccl,out test)
   with
     SubtermUnificationError e ->
       raise (PretypeError (env,sigma,CannotUnifyOccurrences e))
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f315f4445..4d8c97870 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3876,6 +3876,11 @@ let pose_induction_arg clear_flag isrec with_evars info_arg elim
   end
 end
 
+let has_generic_occurrences_but_goal cls id env ccl =
+  clause_with_generic_occurrences cls &&
+  (* TODO: whd_evar of goal *)
+  (cls.concl_occs != NoOccurrences || not (occur_var env id ccl))
+
 let induction_gen clear_flag isrec with_evars elim
     ((_pending,(c,lbind)),(eqname,names) as arg) cls =
   let inhyps = match cls with
@@ -3884,11 +3889,12 @@ let induction_gen clear_flag isrec with_evars elim
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
+  let ccl = Proofview.Goal.raw_concl gl in
   let cls = Option.default allHypsAndConcl cls in
   let t = typ_of env sigma c in
   let is_arg_pure_hyp =
     isVar c && lbind == NoBindings && not with_evars && Option.is_empty eqname
-    && not (has_selected_occurrences cls) in
+    && has_generic_occurrences_but_goal cls (destVar c) env ccl in
   let enough_applied = check_enough_applied env sigma elim t in
   if is_arg_pure_hyp && enough_applied then
     (* First case: induction on a variable already in an inductive type and