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