Ajout de dépliage de l'énoncé, si besoin est, dans apply in

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9363 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 18 insertions, 3 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cc1581296b..f27d116e4a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -562,15 +562,22 @@ let find_matching_clause unifier clause =
     with NotExtensibleClause -> failwith "Cannot apply"
   in find clause
 
-let apply_in_once gls innerclause (d,lbind) =
-  let thm = nf_betaiota (pf_type_of gls d) in
-  let clause = make_clenv_binding gls (d,thm) lbind in
+let progress_with_clause innerclause clause =
   let ordered_metas = List.rev (clenv_independent clause) in
   if ordered_metas = [] then error "Statement without assumptions";
   let f mv = find_matching_clause (clenv_fchain mv clause) innerclause in
   try list_try_find f ordered_metas
   with Failure _ -> error "Unable to unify"
 
+let apply_in_once gls innerclause (d,lbind) =
+  let thm = nf_betaiota (pf_type_of gls d) in
+  let rec aux clause =
+    try progress_with_clause innerclause clause
+    with err ->
+    try aux (clenv_push_prod clause)
+    with NotExtensibleClause -> raise err
+  in aux (make_clenv_binding gls (d,thm) lbind)
+
 let apply_in id lemmas gls =
   let t' = pf_get_hyp_typ gls id in
   let innermostclause = mk_clenv_from_n gls (Some 0) (mkVar id,t') in
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 4f26069633..30fa4129d7 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -12,3 +12,11 @@ Goal forall x y z, ~ z <= 0 -> x * z < y * z -> x <= y.
 intros; apply Znot_le_gt, Zgt_lt in H.
 apply Zmult_lt_reg_r, Zlt_le_weak in H0; auto.
 Qed.
+
+(* Check if it unfolds when there are not enough premises *)
+
+Goal forall n, n = S n -> False.
+intro.
+apply n_Sn in H.
+assumption.
+Qed.