Fixing a bug introduced in the extension of 'apply in' + simplifying code.

2 files changed, 19 insertions, 8 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 83e282a303..407f367ed9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1164,13 +1164,8 @@ let descend_in_conjunctions tac exit c =
 	    match make_projection env sigma params cstr sign elim i n c u with
 	    | None -> Tacticals.New.tclFAIL 0 (mt())
 	    | Some (p,pt) ->
-	    Tacticals.New.tclTHENS
-	      (assert_before Anonymous pt)
-	      [Proofview.V82.tactic (refine p); (* Might be ill-typed due to forbidden elimination. *)
-	       Tacticals.New.onLastHypId (fun id ->
-                 Tacticals.New.tclTHEN
-                   (tac (not isrec) (mkVar id))
-                   (Proofview.V82.tactic (thin [id])))]
+                (* Might be ill-typed due to forbidden elimination. *)
+                tac (not isrec) p
             end))
     | None ->
 	raise Exit
@@ -1344,7 +1339,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
           Tacticals.New.tclTHEN
             (apply_clear_request clear_flag false c)
             (tac id))
-    with e when with_destruct ->
+    with e when with_destruct && when Errors.noncritical e ->
       let e = Errors.push e in
       descend_in_conjunctions aux (fun _ -> raise e) c
     end
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 57b030fc5d..1393843ece 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -446,3 +446,19 @@ Goal forall H:0=0, H = H.
 intros.
 Fail apply eq_sym in H.
 Abort.
+
+(* Check naming pattern in apply in *)
+
+Goal ((False /\ (True -> True))) -> True -> True.
+intros F H.
+apply F in H as H0. (* Check that H0 is not used internally *)
+exact H0.
+Qed.
+
+Goal ((False /\ (True -> True/\True))) -> True -> True/\True.
+intros F H.
+apply F in H as (?,?).
+split.
+exact H. (* Check that generated names are H and H0 *)
+exact H0.
+Qed.