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").

---
 pretyping/locusops.ml  | 11 +++++++++++
 pretyping/locusops.mli |  1 +
 2 files changed, 12 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index cc19f01f80..c5b9c67904 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -103,6 +103,17 @@ let occurrences_of_goal cls =
 let in_every_hyp cls = Option.is_empty cls.onhyps
 
 let clause_with_generic_occurrences cls =
+  let hyps = match cls.onhyps with
+  | 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 ->
diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli
index 1d7c6b72eb..3892271a53 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
-- 
cgit v1.2.3