Mercurial > cpdt > repo
diff src/Match.v @ 204:cbf2f74a5130
Parts I want to keep compile with 8.2
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Fri, 06 Nov 2009 10:52:43 -0500 |
| parents | ce4cc7fa9b2b |
| children | f05514cc6c0d |
line wrap: on
line diff
--- a/src/Match.v Sun Jan 04 08:18:59 2009 -0500 +++ b/src/Match.v Fri Nov 06 10:52:43 2009 -0500 @@ -784,10 +784,10 @@ Ltac matcher := intros; - repeat search_prem ltac:(apply False_prem || (apply ex_prem; intro)); - repeat search_conc ltac:(apply True_conc || eapply ex_conc - || search_prem ltac:(apply Match)); - try apply imp_True. + repeat search_prem ltac:(simple apply False_prem || (simple apply ex_prem; intro)); + repeat search_conc ltac:(simple apply True_conc || simple eapply ex_conc + || search_prem ltac:(simple apply Match)); + try simple apply imp_True. (* end thide *) (** Our tactic succeeds at proving a simple example. *)