Enlarge the cases where the like first selection is used in destruct.

This is now a "like first" strategy iff there is no occurrences
selected in either the goal or in one of the hypotheses possibly given
in an "in" clause. Before, it was "like first" if and only if no "in"
clause was given at all.

1 files changed, 11 insertions, 11 deletions

diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 21157d9d5..7e825b6c2 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -87,22 +87,22 @@ let out_arg = function
   | Misctypes.ArgVar _ -> Errors.anomaly (Pp.str "Unevaluated or_var variable")
   | Misctypes.ArgArg x -> x
 
-let occurrences_of_hyp id =function
-  | LikeFirst -> LikeFirst
-  | AtOccs cls ->
+let occurrences_of_hyp id cls =
   let rec hyp_occ = function
       [] -> NoOccurrences, InHyp
     | ((occs,id'),hl)::_ when Names.Id.equal id id' ->
         occurrences_map (List.map out_arg) occs, hl
     | _::l -> hyp_occ l in
-  AtOccs (match cls.onhyps with
+  match cls.onhyps with
       None -> AllOccurrences,InHyp
-    | Some l -> hyp_occ l)
+    | Some l -> hyp_occ l
 
-let occurrences_of_goal = function
-  | LikeFirst -> LikeFirst
-  | AtOccs cls -> AtOccs (occurrences_map (List.map out_arg) cls.concl_occs)
+let occurrences_of_goal cls =
+  occurrences_map (List.map out_arg) cls.concl_occs
 
-let in_every_hyp = function
-  | LikeFirst -> true
-  | AtOccs cls -> Option.is_empty cls.onhyps
+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)