diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/omega/Zcomplements.v | 8 | ||||
| -rw-r--r-- | contrib/omega/coq_omega.ml | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/contrib/omega/Zcomplements.v b/contrib/omega/Zcomplements.v index 1cbf284a55..67b7751b3f 100644 --- a/contrib/omega/Zcomplements.v +++ b/contrib/omega/Zcomplements.v @@ -70,9 +70,9 @@ Lemma Zlt_Zmult_right : (x,y,z:Z)`z>0` -> `x < y` -> `x*z < y*z`. Intros; Rewrite (Zs_pred z); Generalize (Zgt0_le_pred H); Intro; Apply natlike_ind with P:=[z:Z]`x*(Zs z) < y*(Zs z)`; -[ Simpl; Do 2 (Rewrite Zmult_n_1); Assumption -| Unfold Zs; Intros x0 Hx0; Do 6 (Rewrite Zmult_plus_distr_r); - Repeat (Rewrite Zmult_n_1); +[ Simpl; Do 2 '(Rewrite Zmult_n_1); Assumption +| Unfold Zs; Intros x0 Hx0; Do 6 '(Rewrite Zmult_plus_distr_r); + Repeat Rewrite Zmult_n_1; Intro; Apply Zlt_Zplus; Assumption | Assumption ]. Save. @@ -82,7 +82,7 @@ Intros x y z H; Rewrite (Zs_pred z). Apply natlike_ind with P:=[z:Z]`x*(Zs z) < y*(Zs z)`->`x < y`. Simpl; Do 2 Rewrite Zmult_n_1; Auto 1. Unfold Zs. -Intros x0 Hx0; Repeat (Rewrite Zmult_plus_distr_r). +Intros x0 Hx0; Repeat Rewrite Zmult_plus_distr_r. Repeat Rewrite Zmult_n_1. Omega. Unfold Zpred; Omega. diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index f57a17f30e..dd9b4b1e3a 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -11,7 +11,7 @@ open Util open Pp open Reduction -open Proof_trees +open Proof_type open Ast open Names open Generic |