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.

4 files changed, 30 insertions, 24 deletions

diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 21157d9d5a..7e825b6c24 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)
diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli
index f6d27a1850..c1bf2d9eae 100644
--- a/pretyping/locusops.mli
+++ b/pretyping/locusops.mli
@@ -38,7 +38,8 @@ val concrete_clause_of : (unit -> Id.t list) -> clause -> concrete_clause
 
 (** Miscellaneous functions *)
 
-val occurrences_of_hyp : Id.t -> clause or_like_first ->
-  (occurrences * hyp_location_flag) or_like_first
-val occurrences_of_goal : clause or_like_first -> occurrences or_like_first
-val in_every_hyp : clause or_like_first -> bool
+val occurrences_of_hyp : Id.t -> clause -> (occurrences * hyp_location_flag)
+val occurrences_of_goal : clause -> occurrences
+val in_every_hyp : clause -> bool
+
+val has_selected_occurrences : clause -> bool
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 07940bf57d..3f2963bfe5 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1468,10 +1468,11 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
     else
       x
   in
+  let likefirst = not (has_selected_occurrences occs) in
   let mkvarid () = mkVar id in
   let compute_dependency _ (hyp,_,_ as d) (sign,depdecls) =
     match occurrences_of_hyp hyp occs with
-    | AtOccs (NoOccurrences, InHyp) ->
+    | NoOccurrences, InHyp ->
         if indirectly_dependent c d depdecls then
           (* Told explicitly not to abstract over [d], but it is dependent *)
           let id' = indirect_dependency d depdecls in
@@ -1480,8 +1481,9 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
             ++ str ".")
         else
           (push_named_context_val d sign,depdecls)
-    | (AtOccs (AllOccurrences, InHyp) | LikeFirst) ->
-        let newdecl = replace_term_occ_decl_modulo LikeFirst test mkvarid d in
+    | AllOccurrences, InHyp as occ ->
+        let occ = if likefirst then LikeFirst else AtOccs occ in
+        let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in
         if Context.eq_named_declaration d newdecl
            && not (indirectly_dependent c d depdecls)
         then
@@ -1491,15 +1493,18 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
         else
           (push_named_context_val newdecl sign, newdecl :: depdecls)
     | occ ->
-        let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in
+        (* There are specific occurrences, hence not like first *)
+        let newdecl = replace_term_occ_decl_modulo (AtOccs occ) test mkvarid d in
         (push_named_context_val newdecl sign, newdecl :: depdecls) in
   try
     let sign,depdecls =
       fold_named_context compute_dependency env
         ~init:(empty_named_context_val,[]) in
     let ccl = match occurrences_of_goal occs with
-      | AtOccs NoOccurrences -> concl
-      | occ -> replace_term_occ_modulo occ test mkvarid concl
+      | NoOccurrences -> concl
+      | occ ->
+          let occ = if likefirst then LikeFirst else AtOccs occ in
+          replace_term_occ_modulo occ test mkvarid concl
     in
     let lastlhyp =
       if List.is_empty depdecls then None else Some (pi1(List.last depdecls)) in
@@ -1522,7 +1527,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
 type prefix_of_inductive_support_flag = bool
 
 type abstraction_request =
-| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * pending_constr * clause or_like_first * bool
+| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * pending_constr * clause * bool
 | AbstractExact of Name.t * constr * types option * clause * bool
 
 type abstraction_result =
@@ -1539,7 +1544,7 @@ let make_abstraction env evd ccl abs =
   | AbstractExact (name,c,ty,occs,check_occs) ->
       make_abstraction_core name
         (make_eq_test env evd c)
-        env evd c ty (AtOccs occs) check_occs ccl
+        env evd c ty occs check_occs ccl
 
 let keyed_unify env evd kop = 
   if not !keyed_unification then fun cl -> true
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 7f5cac2d23..0f5a62bb5f 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -68,7 +68,7 @@ exception PatternNotFound
 type prefix_of_inductive_support_flag = bool
 
 type abstraction_request =
-| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * pending_constr * Locus.clause Locus.or_like_first * bool
+| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * pending_constr * Locus.clause * bool
 | AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool
 
 val finish_evar_resolution : ?flags:Pretyping.inference_flags ->