From fc38a7d8f3d2a47aa8eee570747568335f3ffa19 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Wed, 3 May 2000 17:31:07 +0000
Subject: Ajout du langage de tactiques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/omega/Zcomplements.v | 8 ++++----
 contrib/omega/coq_omega.ml   | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'contrib')

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
-- 
cgit v1.2.3