diff options
| -rw-r--r-- | tactics/tactics.ml | 11 | ||||
| -rw-r--r-- | test-suite/success/apply.v | 16 |
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. |