MAJ pour Reg

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3615 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 12 insertions, 15 deletions

diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v
index 6346fc2ee..4010f1d44 100644
--- a/theories/Reals/NewtonInt.v
+++ b/theories/Reals/NewtonInt.v
@@ -90,8 +90,8 @@ Left; Unfold antiderivative; Unfold antiderivative in H H0; Elim H; Clear H; Int
 Split.
 Intros; Elim (H ? H2); Elim (H0 ? H2); Intros.
 Assert H5 : (derivable_pt [y:R]``l*(x y)+(x0 y)`` x1).
-Reg ().
-Exists H5; Symmetry; Reg (); Rewrite <- H3; Rewrite <- H4; Reflexivity.
+Reg.
+Exists H5; Symmetry; Reg; Rewrite <- H3; Rewrite <- H4; Reflexivity.
 Assumption.
 Unfold antiderivative in H H0; Elim H; Elim H0; Intros; Elim H4; Intro.
 Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? H5 H2)).
@@ -107,8 +107,8 @@ Unfold derivable_pt; Exists (f x1); Elim (H3 ? H10); Intros; EApply derive_pt_eq
 Assert H13 : (derivable_pt x0 x1).
 Unfold derivable_pt; Exists (g x1); Elim (H1 ? H11); Intros; EApply derive_pt_eq_1; Symmetry; Apply H13.
 Assert H14 : (derivable_pt [y:R]``l*(x y)+(x0 y)`` x1).
-Reg ().
-Exists H14; Symmetry; Reg ().
+Reg.
+Exists H14; Symmetry; Reg.
 Assert H15 : ``(derive_pt x0 x1 H13)==(g x1)``.
 Elim (H1 ? H11); Intros; Rewrite H15; Apply pr_nu.
 Assert H16 : ``(derive_pt x x1 H12)==(f x1)``.
@@ -130,8 +130,8 @@ Unfold derivable_pt; Exists (f x1); Elim (H3 ? H11); Intros; EApply derive_pt_eq
 Assert H13 : (derivable_pt x0 x1).
 Unfold derivable_pt; Exists (g x1); Elim (H1 ? H10); Intros; EApply derive_pt_eq_1; Symmetry; Apply H13.
 Assert H14 : (derivable_pt [y:R]``l*(x y)+(x0 y)`` x1).
-Reg ().
-Exists H14; Symmetry; Reg ().
+Reg.
+Exists H14; Symmetry; Reg.
 Assert H15 : ``(derive_pt x0 x1 H13)==(g x1)``.
 Elim (H1 ? H10); Intros; Rewrite H15; Apply pr_nu.
 Assert H16 : ``(derive_pt x x1 H12)==(f x1)``.
@@ -141,8 +141,8 @@ Right; Reflexivity.
 Right; Unfold antiderivative; Unfold antiderivative in H H0; Elim H; Clear H; Intros; Elim H0; Clear H0; Intros H0 _; Split.
 Intros; Elim (H ? H2); Elim (H0 ? H2); Intros.
 Assert H5 : (derivable_pt [y:R]``l*(x y)+(x0 y)`` x1).
-Reg ().
-Exists H5; Symmetry; Reg (); Rewrite <- H3; Rewrite <- H4; Reflexivity.
+Reg.
+Exists H5; Symmetry; Reg; Rewrite <- H3; Rewrite <- H4; Reflexivity.
 Assumption.
 Defined.
 
@@ -151,8 +151,8 @@ Lemma antiderivative_P1 : (f,g,F,G:R->R;l,a,b:R) (antiderivative f F a b) -> (an
 Unfold antiderivative; Intros; Elim H; Elim H0; Clear H H0; Intros; Split.
 Intros; Elim (H ? H3); Elim (H1 ? H3); Intros.
 Assert H6 : (derivable_pt [x:R]``l*(F x)+(G x)`` x).
-Reg ().
-Exists H6; Symmetry; Reg (); Rewrite <- H4; Rewrite <- H5; Ring.
+Reg.
+Exists H6; Symmetry; Reg; Rewrite <- H4; Rewrite <- H5; Ring.
 Assumption.
 Qed.
 
diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v
index 17d9ea08f..2575b8508 100644
--- a/theories/Reals/Ranalysis.v
+++ b/theories/Reals/Ranalysis.v
@@ -456,7 +456,7 @@ Match trm With
 | _ -> Idtac.
 
 (**********)
-Tactic Definition Regularity () :=
+Tactic Definition Reg :=
 Match Context With
 | [|-(derivable_pt ?1 ?2)] -> 
 Let trm = Eval Cbv Beta in (?1 AppVar) In
@@ -473,7 +473,4 @@ Let aux = (RewTerm trm) In IntroHypL aux ?2; Try (Change (continuity_pt aux ?2);
 | [|-(eqT ? (derive_pt ?1 ?2 ?3) ?4)] -> 
 Let trm = Eval Cbv Beta in (?1 AppVar) In
 Let aux = (RewTerm trm) In
-IntroHypL aux ?2; Let aux2 = (ConsProof aux ?2) In Try (Replace (derive_pt ?1 ?2 ?3) with (derive_pt aux ?2 aux2); [SimplifyDerive aux ?2; Try Unfold plus_fct minus_fct mult_fct div_fct id fct_cte inv_fct opp_fct; Try Ring | Try Apply pr_nu]) Orelse IsDiff_pt.
-
-(**********)
-Tactic Definition Reg () := Regularity ().
+IntroHypL aux ?2; Let aux2 = (ConsProof aux ?2) In Try (Replace (derive_pt ?1 ?2 ?3) with (derive_pt aux ?2 aux2); [SimplifyDerive aux ?2; Try Unfold plus_fct minus_fct mult_fct div_fct id fct_cte inv_fct opp_fct; Try Ring | Try Apply pr_nu]) Orelse IsDiff_pt.
\ No newline at end of file