diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-31 17:29:49 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-31 18:49:05 +0100 |
| commit | 1177da32723fd46a82b66ca7ffe4d13d93480da6 (patch) | |
| tree | 8d66f89beafc497e529bdcefd2372bdd23d90cba /pretyping/locusops.ml | |
| parent | 801cd9cb0559d3b78216da166044bd02348ed9af (diff) | |
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.
Diffstat (limited to 'pretyping/locusops.ml')
| -rw-r--r-- | pretyping/locusops.ml | 14 |
1 files changed, 10 insertions, 4 deletions
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 |