diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-07-03 16:19:56 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-07-03 16:19:56 +0000 |
| commit | 9013e6d80b26b177fbcd10a706f271ca4b576585 (patch) | |
| tree | d2c1629768786116e6a5dec36fcda457d2a48ea8 | |
| parent | 1993e7d72cb84d8a71083fd537ada3e12fc39392 (diff) | |
Opaque pas encore implementee; syntax langage tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@552 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/omega/Zlogarithm.v | 3 | ||||
| -rw-r--r-- | contrib/omega/Zpower.v | 2 |
2 files changed, 4 insertions, 1 deletions
diff --git a/contrib/omega/Zlogarithm.v b/contrib/omega/Zlogarithm.v index c5b36397f..803981e33 100644 --- a/contrib/omega/Zlogarithm.v +++ b/contrib/omega/Zlogarithm.v @@ -14,6 +14,7 @@ (* (Log_nearest x) is the integer nearest from (Log x). *) (****************************************************************************) +Require ZArith. Require Omega. Require Zcomplements. Require Zpower. @@ -67,7 +68,9 @@ Definition log_inf_correct1 := Definition log_inf_correct2 := [p:positive](proj2 ? ? (log_inf_correct p)). +(***TODO: retablir les commandes Opaque / Transparent Opaque log_inf_correct1 log_inf_correct2. +***) Hints Resolve log_inf_correct1 log_inf_correct2 : zarith. Lemma log_sup_correct1 : (p:positive)` 0 <= (log_sup p)`. diff --git a/contrib/omega/Zpower.v b/contrib/omega/Zpower.v index d56e607d5..c696aec28 100644 --- a/contrib/omega/Zpower.v +++ b/contrib/omega/Zpower.v @@ -344,7 +344,7 @@ Intros; Apply iter_pos_invariant with [ Intro; Rewrite NEG_xI; Unfold Zminus; Intro; Elim H; Intros; Split; [ Rewrite H0; Rewrite Zplus_assoc; Apply f_equal with f:=[z:Z]`z+r`; - Do 2 (Rewrite Zmult_plus_distr_l); + Do 2 '(Rewrite Zmult_plus_distr_l); Rewrite Zmult_assoc; Rewrite (Zmult_sym (NEG p1) `2`); Rewrite <- Zplus_assoc; |