Fixing 1177da327 (reorganization of the test for generic selection of

occurrences: some uniformisation was not appropriate for "change").

1 files changed, 11 insertions, 0 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