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.

6 files changed, 81 insertions, 57 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 ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6ce360919c..f315f44455 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2255,7 +2255,7 @@ let letin_pat_tac with_eq id c occs =
     let sigma = Proofview.Goal.sigma gl in
     let ccl = Proofview.Goal.concl gl in
     let check t = true in
-    let abs = AbstractPattern (false,check,id,c,AtOccs occs,false) in
+    let abs = AbstractPattern (false,check,id,c,occs,false) in
     let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in
     let sigma,c = match res with
     | None -> finish_evar_resolution ~flags:(tactic_infer_flags false) env sigma c
@@ -3747,34 +3747,24 @@ let induction_without_atomization isrec with_evars elim names lid =
       (induction_from_context_l with_evars elim_info lid names)
   end
 
-let has_selected_occurrences = function
-  | None -> false
-  | Some cls ->
-      cls.concl_occs != AllOccurrences ||
-	not (Option.is_empty cls.onhyps) && List.exists (fun ((occs,_),hl) ->
-          occs != AllOccurrences || hl != InHyp) (Option.get cls.onhyps)
-
 (* assume that no occurrences are selected *)
 let clear_unselected_context id inhyps cls gl =
-  match cls with
+  if occur_var (pf_env gl) id (pf_concl gl) &&
+    cls.concl_occs == NoOccurrences
+  then errorlabstrm ""
+    (str "Conclusion must be mentioned: it depends on " ++ pr_id id
+     ++ str ".");
+  match cls.onhyps with
+  | Some hyps ->
+      let to_erase (id',_,_ as d) =
+	if Id.List.mem id' inhyps then (* if selected, do not erase *) None
+	else
+	  (* erase if not selected and dependent on id or selected hyps *)
+	  let test id = occur_var_in_decl (pf_env gl) id d in
+	  if List.exists test (id::inhyps) then Some id' else None in
+      let ids = List.map_filter to_erase (pf_hyps gl) in
+      thin ids gl
   | None -> tclIDTAC gl
-  | Some cls ->
-      if occur_var (pf_env gl) id (pf_concl gl) &&
-	 cls.concl_occs == NoOccurrences
-      then errorlabstrm ""
-	    (str "Conclusion must be mentioned: it depends on " ++ pr_id id
-	     ++ str ".");
-      match cls.onhyps with
-      | Some hyps ->
-	  let to_erase (id',_,_ as d) =
-	    if Id.List.mem id' inhyps then (* if selected, do not erase *) None
-	    else
-	      (* erase if not selected and dependent on id or selected hyps *)
-	      let test id = occur_var_in_decl (pf_env gl) id d in
-	      if List.exists test (id::inhyps) then Some id' else None in
-	  let ids = List.map_filter to_erase (pf_hyps gl) in
-	  thin ids gl
-      | None -> tclIDTAC gl
 
 let use_bindings env sigma (c,lbind) typ =
   (* We don't try to normalize the type to an inductive type because *)
@@ -3864,9 +3854,8 @@ let pose_induction_arg clear_flag isrec with_evars info_arg elim
   let ccl = Proofview.Goal.concl gl in
   Proofview.Refine.refine ~unsafe:true begin fun sigma ->
   let (sigma',c') = use_bindings env sigma (c0,lbind) t0 in
-  let occs = match cls with None -> LikeFirst | Some occs -> AtOccs occs in
   let check = check_enough_applied env sigma elim in
-  let abs = AbstractPattern (snd info_arg,check,Name id,(pending,c'),occs,false) in
+  let abs = AbstractPattern (snd info_arg,check,Name id,(pending,c'),cls,false) in
   let (id,sign,_,lastlhyp,ccl,res) = make_abstraction env sigma' ccl abs in
   match res with
   | None ->
@@ -3895,6 +3884,7 @@ let induction_gen clear_flag isrec with_evars elim
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
+  let cls = Option.default allHypsAndConcl cls in
   let t = typ_of env sigma c in
   let is_arg_pure_hyp =
     isVar c && lbind == NoBindings && not with_evars && Option.is_empty eqname
@@ -4064,7 +4054,7 @@ let induction_destruct isrec with_evars (lc,elim) =
       let lc = List.map (on_pi1 (map_induction_arg finish_evar_resolution)) lc in
       let newlc =
         List.map (fun (x,(eqn,names),cls) ->
-          if cls <> None then error "'in' clause not yet supported here.";
+          if cls != None then error "'in' clause not yet supported here.";
 	  match x with (* FIXME: should we deal with ElimOnIdent? *)
           | _clear_flag,ElimOnConstr x ->
               if eqn <> None then error "'eqn' clause not supported here.";
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 56ec6a02d6..5f94d8e722 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -256,9 +256,9 @@ Qed.
 (* Check destruct on idents with maximal implicit arguments - which did
    not work in 8.4 *)
 
-Parameter f : forall {n:nat}, n=n -> nat.
-Goal f (eq_refl 0) = 0.
-destruct f.
+Parameter g : forall {n:nat}, n=n -> nat.
+Goal g (eq_refl 0) = 0.
+destruct g.
 Abort.
 
 (* This one was working in 8.4 (because of full conv on closed arguments) *)
@@ -278,7 +278,7 @@ Goal forall f : A -> nat -> nat, f a 0 = f a 1.
 intros.
 destruct f.
 
-(* This one was not working in 8.4 *)
+(* This was not working in 8.4 *)
 
 Section S1.
 Variables x y : Type.
@@ -290,6 +290,34 @@ change (x=y) in H.
 Abort.
 End S1.
 
+(* This was not working in 8.4 *)
+
+Goal forall g:nat->nat, g 0 = g 1 -> g 1 = g 2 -> g 0 = g 2.
+intros.
+induction g.
+2:change (n = g 1 -> n = g 2) in IHn.
+Abort.
+
+(* This was not working in 8.4 *)
+
+Goal forall g:nat->nat, g 0 = g 1 -> g 1 = g 2 -> g 0 = g 2. 
+intros g H H0.
+induction g in H |- *.
+Abort.
+
+(* "at" was not granted in 8.4 in the next two examples *)
+
+Goal forall g:nat->nat, g 0 = g 1 -> g 1 = g 2 -> g 0 = g 2. 
+intros g H H0.
+induction g in H at 2, H0 at 1.
+change (g 0 = 0) in H.
+Abort.
+
+Goal forall g:nat->nat, g 0 = g 1 -> g 1 = g 2 -> g 0 = g 2. 
+intros g H H0.
+Fail induction g in H at 2 |- *. (* Incompatible occurrences *)
+Abort.
+
 (* These ones are not satisfactory at the current time
 
 Section S2.