diff options
| -rw-r--r-- | pretyping/locusops.ml | 11 | ||||
| -rw-r--r-- | pretyping/locusops.mli | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
3 files changed, 13 insertions, 1 deletions
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index cc19f01f8..c5b9c6790 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -107,6 +107,17 @@ let clause_with_generic_occurrences cls = | None -> true | Some hyps -> List.for_all + (function ((AllOccurrences,_),_) -> true | _ -> false) hyps in + let concl = match cls.concl_occs with + | AllOccurrences | NoOccurrences -> true + | _ -> false in + hyps && concl + +let clause_with_generic_context_selection 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 diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index 1d7c6b72e..3892271a5 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -43,3 +43,4 @@ val occurrences_of_goal : clause -> occurrences val in_every_hyp : clause -> bool val clause_with_generic_occurrences : 'a clause_expr -> bool +val clause_with_generic_context_selection : 'a clause_expr -> bool diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 4d8c97870..23ec74db0 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)) |