diff options
author | 2000-05-03 17:31:07 +0000 | |
---|---|---|
committer | 2000-05-03 17:31:07 +0000 | |
commit | fc38a7d8f3d2a47aa8eee570747568335f3ffa19 (patch) | |
tree | 9ddc595a02cf1baaab3e9595d77b0103c80d66bf /contrib/omega | |
parent | 5b0f516e7e1f6d2ea8ca0485ffe347a613b01a5c (diff) |
Ajout du langage de tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/omega')
-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 1cbf284a5..67b7751b3 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 f57a17f30..dd9b4b1e3 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 |