diff options
| author |  bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-12-11 18:46:35 +0000 |
|---|---|---|
| committer | bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-12-11 18:46:35 +0000 |
| commit | c86d78c0f18fb28f74bb6b192c03ebe73117cf03 (patch) | |
| tree | 99294164215016607e4056e5730a2d6c91043dbf /theories/Reals/Rtrigo.v | |
| parent | 70c88a5f6d7e1ef184d70512969a6221eec8d11e (diff) | |
Changement dans le kernel :
- essai de suppression des dependances debiles. (echec)
- Application des patch debian.
Pour ring et field :
- introduciton de la function de sign et de puissance.
- Correction de certains bug.
- supression de ring_replace ....
Pour exact_no_check :
- ajout de la tactic : vm_cast_no_check (t)
qui remplace "exact_no_check (t<: type of Goal)"
(cette version forcais l'evaluation du cast dans le
pretypage).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo.v')
| -rw-r--r-- | theories/Reals/Rtrigo.v | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index d05fd99cb..2adac468b 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -1580,10 +1580,14 @@ Lemma cos_eq_0_0 : Proof. intros x H; rewrite cos_sin in H; generalize (sin_eq_0_0 (PI / INR 2 + x) H); intro H2; elim H2; intros x0 H3; exists (x0 - Z_of_nat 1)%Z; - rewrite <- Z_R_minus; simpl; ring_simplify; -(* rewrite (Rmult_comm PI);*) (* old ring compat *) + rewrite <- Z_R_minus; simpl. +unfold INR in H3. field_simplify [(sym_eq H3)]. field. +(** + ring_simplify. + (* rewrite (Rmult_comm PI);*) (* old ring compat *) rewrite <- H3; simpl; - field; repeat split; discrR. + field;repeat split; discrR. +*) Qed. Lemma cos_eq_0_1 : |