Nommage explicite des hypotheses introduites quand le nom existe aussi comme global

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

4 files changed, 57 insertions, 57 deletions

diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v
index 520ccc788a..3e2ff2bb7d 100644
--- a/theories/Reals/MVT.v
+++ b/theories/Reals/MVT.v
@@ -107,7 +107,7 @@ Qed.
 
 (* Corollaries ... *)
 Lemma MVT_cor1 : (f:(R->R); a,b:R; pr:(derivable f)) ``a < b``->(EXT c:R | ``(f b)-(f a) == (derive_pt f c (pr c))*(b-a)``/\``a < c < b``).
-Intros; Cut (c:R)``a<c<b``->(derivable_pt f c); [Intro | Intros; Apply pr].
+Intros f a b pr H; Cut (c:R)``a<c<b``->(derivable_pt f c); [Intro | Intros; Apply pr].
 Cut (c:R)``a<c<b``->(derivable_pt id c); [Intro | Intros; Apply derivable_pt_id].
 Cut ((c:R)``a<=c<=b``->(continuity_pt f c)); [Intro | Intros; Apply derivable_continuous_pt; Apply pr].
 Cut ((c:R)``a<=c<=b``->(continuity_pt id c)); [Intro | Intros; Apply derivable_continuous_pt; Apply derivable_id].
@@ -120,7 +120,7 @@ Apply x.
 Qed.
 
 Theorem MVT_cor2 : (f,f':R->R;a,b:R) ``a<b`` -> ((c:R)``a<=c<=b``->(derivable_pt_lim f c (f' c))) -> (EXT c:R | ``(f b)-(f a)==(f' c)*(b-a)``/\``a<c<b``).
-Intros; Cut ((c:R)``a<=c<=b``->(derivable_pt f c)).
+Intros f f' a b H H0; Cut ((c:R)``a<=c<=b``->(derivable_pt f c)).
 Intro; Cut ((c:R)``a<c<b``->(derivable_pt f c)).
 Intro; Cut ((c:R)``a<=c<=b``->(continuity_pt f c)).
 Intro; Cut ((c:R)``a<=c<=b``->(derivable_pt id c)).
@@ -142,7 +142,7 @@ Intros; Unfold derivable_pt; Apply Specif.existT with (f' c); Apply H0; Apply H1
 Qed.
 
 Lemma MVT_cor3 : (f,f':(R->R); a,b:R) ``a < b``  -> ((x:R)``a <= x`` ->  ``x <= b``->(derivable_pt_lim f x (f' x))) -> (EXT c:R | ``a<=c``/\``c<=b``/\``(f b)==(f a) + (f' c)*(b-a)``).
-Intros; Assert H1 : (EXT c:R | ``(f b) -(f a) == (f' c)*(b-a)``/\``a<c<b``); [Apply MVT_cor2; [Apply H | Intros; Elim H1; Intros; Apply (H0 ? H2 H3)] | Elim H1; Intros; Exists x; Elim H2; Intros; Elim H4; Intros; Split; [Left; Assumption | Split; [Left; Assumption | Rewrite <- H3; Ring]]].
+Intros f f' a b H H0; Assert H1 : (EXT c:R | ``(f b) -(f a) == (f' c)*(b-a)``/\``a<c<b``); [Apply MVT_cor2; [Apply H | Intros; Elim H1; Intros; Apply (H0 ? H2 H3)] | Elim H1; Intros; Exists x; Elim H2; Intros; Elim H4; Intros; Split; [Left; Assumption | Split; [Left; Assumption | Rewrite <- H3; Ring]]].
 Qed.
 
 Lemma Rolle : (f:R->R;a,b:R;pr:(x:R)``a<x<b``->(derivable_pt f x)) ((x:R)``a<=x<=b``->(continuity_pt f x)) -> ``a<b`` -> (f a)==(f b) -> (EXT c:R | (EXT P: ``a<c<b`` | ``(derive_pt f c (pr c P))==0``)).
@@ -177,7 +177,7 @@ Qed.
  
 (**********)
 Lemma nonpos_derivative_0 : (f:R->R;pr:(derivable f)) (decreasing f) -> ((x:R) ``(derive_pt f x (pr x))<=0``).
-Intros; Assert H0 :=H; Unfold decreasing in H0; Generalize (derivable_derive f x (pr x)); Intro; Elim H1; Intros l H2.
+Intros f pr H x; Assert H0 :=H; Unfold decreasing in H0; Generalize (derivable_derive f x (pr x)); Intro; Elim H1; Intros l H2.
 Rewrite H2; Case (total_order l R0); Intro.
 Left; Assumption.
 Elim H3; Intro.
@@ -413,7 +413,7 @@ Qed.
 
 (**********)
 Lemma derive_increasing_interv_var : (a,b:R;f:R->R;pr:(derivable f)) ``a<b``-> ((t:R) ``a<t<b`` -> ``0<=(derive_pt f t (pr t))``) -> ((x,y:R) ``a<=x<=b``->``a<=y<=b``->``x<y``->``(f x)<=(f y)``).
-Intros; Generalize (derive_increasing_interv_ax a b f pr H); Intro; Elim H4; Intros _ H5; Apply (H5 H0 x y H1 H2 H3).
+Intros a b f pr H H0 x y H1 H2 H3; Generalize (derive_increasing_interv_ax a b f pr H); Intro; Elim H4; Intros _ H5; Apply (H5 H0 x y H1 H2 H3).
 Qed.
 
 (**********)
diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v
index b0d0d5949d..8f7a4fa11e 100644
--- a/theories/Reals/NewtonInt.v
+++ b/theories/Reals/NewtonInt.v
@@ -25,7 +25,7 @@ Definition NewtonInt [f:R->R;a,b:R;pr:(Newton_integrable f a b)] : R := let g =
 
 (* If f is differentiable, then f' is Newton integrable (Tautology ?) *)
 Lemma FTCN_step1 : (f:Differential;a,b:R) (Newton_integrable [x:R](derive_pt f x (cond_diff f x)) a b).
-Intros; Unfold Newton_integrable; Apply existTT with (d1 f); Unfold antiderivative; Intros; Case (total_order_Rle a b); Intro; [Left; Split; [Intros; Exists (cond_diff f x); Reflexivity | Assumption] | Right; Split; [Intros; Exists (cond_diff f x); Reflexivity | Auto with real]].
+Intros f a b; Unfold Newton_integrable; Apply existTT with (d1 f); Unfold antiderivative; Intros; Case (total_order_Rle a b); Intro; [Left; Split; [Intros; Exists (cond_diff f x); Reflexivity | Assumption] | Right; Split; [Intros; Exists (cond_diff f x); Reflexivity | Auto with real]].
 Defined.
 
 (* By definition, we have the Fondamental Theorem of Calculus *)
@@ -35,7 +35,7 @@ Qed.
 
 (* $\int_a^a f$ exists forall a:R and f:R->R *)
 Lemma NewtonInt_P1 : (f:R->R;a:R) (Newton_integrable f a a).
-Intros; Unfold Newton_integrable; Apply existTT with (mult_fct (fct_cte (f a)) id); Left; Unfold antiderivative; Split.
+Intros f a; Unfold Newton_integrable; Apply existTT with (mult_fct (fct_cte (f a)) id); Left; Unfold antiderivative; Split.
 Intros; Assert H1 : (derivable_pt (mult_fct (fct_cte (f a)) id) x).
 Apply derivable_pt_mult.
 Apply derivable_pt_const.
@@ -159,7 +159,7 @@ Qed.
 
 (* $\int_a^b \lambda f + g = \lambda \int_a^b f + \int_a^b f *)
 Lemma NewtonInt_P6 : (f,g:R->R;l,a,b:R;pr1:(Newton_integrable f a b);pr2:(Newton_integrable g a b)) (NewtonInt [x:R]``l*(f x)+(g x)`` a b (NewtonInt_P5 f g l a b pr1 pr2))==``l*(NewtonInt f a b pr1)+(NewtonInt g a b pr2)``.
-Intros; Unfold NewtonInt; Case (NewtonInt_P5 f g l a b pr1 pr2); Intros; Case pr1; Intros; Case pr2; Intros; Case (total_order_T a b); Intro.
+Intros f g l a b pr1 pr2; Unfold NewtonInt; Case (NewtonInt_P5 f g l a b pr1 pr2); Intros; Case pr1; Intros; Case pr2; Intros; Case (total_order_T a b); Intro.
 Elim s; Intro.
 Elim o; Intro.
 Elim o0; Intro.
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v
index b10b1407e9..7966d9c88b 100644
--- a/theories/Reals/RiemannInt.v
+++ b/theories/Reals/RiemannInt.v
@@ -89,11 +89,11 @@ Elim n2; Assumption.
 Qed.
 
 Lemma RiemannInt_exists : (f:R->R;a,b:R;pr:(Riemann_integrable f a b);un:nat->posreal) (Un_cv un R0) -> (sigTT ? [l:R](Un_cv [N:nat](RiemannInt_SF (phi_sequence un pr N)) l)).
-Intros; Apply RiemannInt_P3 with f un [n:nat](projT1 ? ? (phi_sequence_prop un pr n)); [Apply H | Intro; Apply (projT2 ? ? (phi_sequence_prop un pr n))].
+Intros f; Intros; Apply RiemannInt_P3 with f un [n:nat](projT1 ? ? (phi_sequence_prop un pr n)); [Apply H | Intro; Apply (projT2 ? ? (phi_sequence_prop un pr n))].
 Qed.
 
 Lemma RiemannInt_P4 : (f:R->R;a,b,l:R;pr1,pr2:(Riemann_integrable f a b);un,vn:nat->posreal) (Un_cv un R0) -> (Un_cv vn R0) -> (Un_cv [N:nat](RiemannInt_SF (phi_sequence un pr1 N)) l) -> (Un_cv [N:nat](RiemannInt_SF (phi_sequence vn pr2 N)) l).
-Unfold Un_cv; Unfold R_dist; Intros; Assert H3 : ``0<eps/3``.
+Unfold Un_cv; Unfold R_dist; Intros f; Intros; Assert H3 : ``0<eps/3``.
 Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0].
 Elim (H ? H3); Clear H; Intros N0 H; Elim (H0 ? H3); Clear H0; Intros N1 H0; Elim (H1 ? H3); Clear H1; Intros N2 H1; Pose N := (max (max N0 N1) N2); Exists N; Intros; Apply Rle_lt_trans with ``(Rabsolu ((RiemannInt_SF [(phi_sequence vn pr2 n)])-(RiemannInt_SF [(phi_sequence un pr1 n)])))+(Rabsolu ((RiemannInt_SF [(phi_sequence un pr1 n)])-l))``.
 Replace ``(RiemannInt_SF [(phi_sequence vn pr2 n)])-l`` with ``((RiemannInt_SF [(phi_sequence vn pr2 n)])-(RiemannInt_SF [(phi_sequence un pr1 n)]))+((RiemannInt_SF [(phi_sequence un pr1 n)])-l)``; [Apply Rabsolu_triang | Ring].
@@ -223,7 +223,7 @@ Definition max_N [a,b:R;del:posreal;h:``a<b``] : nat := Cases (maxN del h) of (e
 Definition SubEqui [a,b:R;del:posreal;h:``a<b``] :Rlist := (SubEquiN (S (max_N del h)) a b del).
 
 Lemma Heine_cor1 : (f:R->R;a,b:R) ``a<b`` -> ((x:R)``a<=x<=b``->(continuity_pt f x)) -> (eps:posreal) (sigTT ? [delta:posreal]``delta<=b-a``/\(x,y:R)``a<=x<=b``->``a<=y<=b``->``(Rabsolu (x-y)) < delta``->``(Rabsolu ((f x)-(f y))) < eps``).
-Intros; Pose E := [l:R]``0<l<=b-a``/\(x,y:R)``a <= x <= b``->``a <= y <= b``->``(Rabsolu (x-y)) < l``->``(Rabsolu ((f x)-(f y))) < eps``; Assert H1 : (bound E).
+Intro f; Intros; Pose E := [l:R]``0<l<=b-a``/\(x,y:R)``a <= x <= b``->``a <= y <= b``->``(Rabsolu (x-y)) < l``->``(Rabsolu ((f x)-(f y))) < eps``; Assert H1 : (bound E).
 Unfold bound; Exists ``b-a``; Unfold is_upper_bound; Intros; Unfold E in H1; Elim H1; Clear H1; Intros H1 _; Elim H1; Intros; Assumption.
 Assert H2 : (EXT x:R | (E x)).
 Assert H2 := (Heine f [x:R]``a<=x<=b`` (compact_P3 a b) H0 eps); Elim H2; Intros; Exists (Rmin x ``b-a``); Unfold E; Split; [Split; [Unfold Rmin; Case (total_order_Rle x ``b-a``); Intro; [Apply (cond_pos x) | Apply Rlt_Rminus; Assumption] | Apply Rmin_r] | Intros; Apply H3; Try Assumption; Apply Rlt_le_trans with (Rmin x ``b-a``); [Assumption | Apply Rmin_l]].
@@ -245,7 +245,7 @@ Apply H5; Intros; Unfold E in H6; Elim H6; Clear H6; Intros H6 _; Elim H6; Intro
 Qed.
 
 Lemma Heine_cor2 : (f:(R->R); a,b:R) ((x:R)``a <= x <= b``->(continuity_pt f x))->(eps:posreal)(sigTT posreal [delta:posreal]((x,y:R)``a <= x <= b``->``a <= y <= b``->``(Rabsolu (x-y)) < delta``->``(Rabsolu ((f x)-(f y))) < eps``)).
-Intros; Case (total_order_T a b); Intro.
+Intro f; Intros; Case (total_order_T a b); Intro.
 Elim s; Intro.
 Assert H0 := (Heine_cor1 a0 H eps); Elim H0; Intros; Apply existTT with x; Elim p; Intros; Apply H2; Assumption.
 Apply existTT with (mkposreal ? Rlt_R0_R1); Intros; Assert H3 : x==y; [Elim H0; Elim H1; Intros; Rewrite b0 in H3; Rewrite b0 in H5; Apply Rle_antisym; Apply Rle_trans with b; Assumption | Rewrite H3; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Apply (cond_pos eps)].
@@ -384,7 +384,7 @@ Apply le_lt_n_Sm; Assumption.
 Qed.
 
 Lemma RiemannInt_P7 : (f:R->R;a:R) (Riemann_integrable f a a).
-Unfold Riemann_integrable; Intros; Split with (mkStepFun (StepFun_P4 a a (f a))); Split with (mkStepFun (StepFun_P4 a a R0)); Split.
+Unfold Riemann_integrable; Intro f; Intros; Split with (mkStepFun (StepFun_P4 a a (f a))); Split with (mkStepFun (StepFun_P4 a a R0)); Split.
 Intros; Simpl; Unfold fct_cte; Replace t with a.
 Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Right; Reflexivity.
 Generalize H; Unfold Rmin Rmax; Case (total_order_Rle a a); Intros; Elim H0; Intros; Apply Rle_antisym; Assumption.
@@ -396,7 +396,7 @@ Intros; Case (total_order_T a b); Intro; [Elim s; Intro; [Apply RiemannInt_P6; A
 Qed.
 
 Lemma RiemannInt_P8 : (f:R->R;a,b:R;pr1:(Riemann_integrable f a b);pr2:(Riemann_integrable f b a)) ``(RiemannInt pr1)==-(RiemannInt pr2)``.
-Intros; EApply UL_sequence.
+Intro f; Intros; EApply UL_sequence.
 Unfold RiemannInt; Case (RiemannInt_exists pr1 5!RinvN RinvN_cv); Intros; Apply u.
 Unfold RiemannInt; Case (RiemannInt_exists pr2 5!RinvN RinvN_cv); Intros; Cut (EXT psi1:nat->(StepFun a b) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((f t)-([(phi_sequence RinvN pr1 n)] t)))<= (psi1 n t)``)/\``(Rabsolu (RiemannInt_SF (psi1 n))) < (RinvN n)``).
 Cut (EXT psi2:nat->(StepFun b a) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((f t)-([(phi_sequence RinvN pr2 n)] t)))<= (psi2 n t)``)/\``(Rabsolu (RiemannInt_SF (psi2 n))) < (RinvN n)``).
@@ -463,7 +463,7 @@ Qed.
 
 (* L1([a,b]) is a vectorial space *)
 Lemma RiemannInt_P10 : (f,g:R->R;a,b,l:R) (Riemann_integrable f a b) -> (Riemann_integrable g a b) -> (Riemann_integrable [x:R]``(f x)+l*(g x)`` a b).
-Unfold Riemann_integrable; Intros; Case (Req_EM_T l R0); Intro.
+Unfold Riemann_integrable; Intros f g; Intros; Case (Req_EM_T l R0); Intro.
 Elim (X eps); Intros; Split with x; Elim p; Intros; Split with x0; Elim p0; Intros; Split; Try Assumption; Rewrite e; Intros; Rewrite Rmult_Ol; Rewrite Rplus_Or; Apply H; Assumption.
 Assert H : ``0<eps/2``.
 Unfold Rdiv; Apply Rmult_lt_pos; [Apply (cond_pos eps) | Apply Rlt_Rinv; Sup0].
@@ -483,7 +483,7 @@ Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym; [Rewrite Rmult_1l; Replace ``/(Ra
 Qed.
 
 Lemma RiemannInt_P11 : (f:R->R;a,b,l:R;un:nat->posreal;phi1,phi2,psi1,psi2:nat->(StepFun a b)) (Un_cv un R0) -> ((n:nat)((t:R)``(Rmin a b)<=t<=(Rmax a b)``->``(Rabsolu ((f t)-(phi1 n t)))<=(psi1 n t)``)/\``(Rabsolu (RiemannInt_SF (psi1 n)))<(un n)``) -> ((n:nat)((t:R)``(Rmin a b)<=t<=(Rmax a b)``->``(Rabsolu ((f t)-(phi2 n t)))<=(psi2 n t)``)/\``(Rabsolu (RiemannInt_SF (psi2 n)))<(un n)``) -> (Un_cv [N:nat](RiemannInt_SF (phi1 N)) l) -> (Un_cv [N:nat](RiemannInt_SF (phi2 N)) l).
-Unfold Un_cv; Intros.
+Unfold Un_cv; Intro f; Intros; Intros.
 Case (total_order_Rle a b); Intro Hyp.
 Assert H4 : ``0<eps/3``.
 Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0].
@@ -595,7 +595,7 @@ Apply r_Rmult_mult with ``3``; [Unfold Rdiv; Rewrite Rmult_Rplus_distr; Do 2 Rew
 Qed.
 
 Lemma RiemannInt_P12 : (f,g:R->R;a,b,l:R;pr1:(Riemann_integrable f a b);pr2:(Riemann_integrable g a b);pr3:(Riemann_integrable [x:R]``(f x)+l*(g x)`` a b)) ``a<=b`` -> ``(RiemannInt pr3)==(RiemannInt pr1)+l*(RiemannInt pr2)``.
-Intros; Case (Req_EM l R0); Intro.
+Intro f; Intros; Case (Req_EM l R0); Intro.
 Pattern 2 l; Rewrite H0; Rewrite Rmult_Ol; Rewrite Rplus_Or; Unfold RiemannInt; Case (RiemannInt_exists pr3 5!RinvN RinvN_cv); Case (RiemannInt_exists pr1 5!RinvN RinvN_cv); Intros; EApply UL_sequence; [Apply u0 | Pose psi1 := [n:nat](projT1 ? ? (phi_sequence_prop RinvN pr1 n)); Pose psi2 := [n:nat](projT1 ? ? (phi_sequence_prop RinvN pr3 n)); Apply RiemannInt_P11 with f RinvN (phi_sequence RinvN pr1) psi1 psi2; [Apply RinvN_cv | Intro; Apply (projT2 ? ? (phi_sequence_prop RinvN pr1 n)) | Intro; Assert H1 : ((t:R) ``(Rmin a b) <= t``/\``t <= (Rmax a b)`` -> (Rle (Rabsolu (Rminus ``(f t)+l*(g t)`` (phi_sequence RinvN pr3 n t))) (psi2 n t))) /\ ``(Rabsolu (RiemannInt_SF (psi2 n))) < (RinvN n)``; [Apply (projT2 ? ? (phi_sequence_prop RinvN pr3 n)) | Elim H1; Intros; Split; Try Assumption; Intros; Replace (f t) with ``(f t)+l*(g t)``; [Apply H2; Assumption | Rewrite H0; Ring]] | Assumption]].
 EApply UL_sequence.
 Unfold RiemannInt; Case (RiemannInt_exists pr3 5!RinvN RinvN_cv); Intros; Apply u.
@@ -684,7 +684,7 @@ Unfold Un_cv; Intros; Split with O; Intros; Unfold R_dist; Unfold phi2; Rewrite
 Qed.
 
 Lemma RiemannInt_P16 : (f:R->R;a,b:R) (Riemann_integrable f a b) -> (Riemann_integrable [x:R](Rabsolu (f x)) a b).
-Unfold Riemann_integrable; Intros; Elim (X eps); Clear X; Intros phi [psi [H H0]]; Split with (mkStepFun (StepFun_P32 phi)); Split with psi; Split; Try Assumption; Intros; Simpl; Apply Rle_trans with ``(Rabsolu ((f t)-(phi t)))``; [Apply Rabsolu_triang_inv2 | Apply H; Assumption].
+Unfold Riemann_integrable; Intro f; Intros; Elim (X eps); Clear X; Intros phi [psi [H H0]]; Split with (mkStepFun (StepFun_P32 phi)); Split with psi; Split; Try Assumption; Intros; Simpl; Apply Rle_trans with ``(Rabsolu ((f t)-(phi t)))``; [Apply Rabsolu_triang_inv2 | Apply H; Assumption].
 Qed.
 
 Lemma Rle_cv_lim : (Un,Vn:nat->R;l1,l2:R) ((n:nat)``(Un n)<=(Vn n)``) -> (Un_cv Un l1) -> (Un_cv Vn l2) -> ``l1<=l2``.
@@ -710,7 +710,7 @@ Apply r_Rmult_mult with ``2``; [Unfold Rdiv; Do 2 Rewrite -> (Rmult_sym ``2``);
 Qed.
 
 Lemma RiemannInt_P17 : (f:R->R;a,b:R;pr1:(Riemann_integrable f a b);pr2:(Riemann_integrable [x:R](Rabsolu (f x)) a b)) ``a<=b`` -> ``(Rabsolu (RiemannInt pr1))<=(RiemannInt pr2)``.
-Intros; Unfold RiemannInt; Case (RiemannInt_exists 1!f 2!a 3!b pr1 5!RinvN RinvN_cv); Case (RiemannInt_exists 1!([x0:R](Rabsolu (f x0))) 2!a 3!b pr2 5!RinvN RinvN_cv); Intros; Pose phi1 := (phi_sequence RinvN pr1); Pose phi2 := [N:nat](mkStepFun (StepFun_P32 (phi1 N))); Apply Rle_cv_lim with [N:nat](Rabsolu (RiemannInt_SF (phi1 N))) [N:nat](RiemannInt_SF (phi2 N)).
+Intro f; Intros; Unfold RiemannInt; Case (RiemannInt_exists 1!f 2!a 3!b pr1 5!RinvN RinvN_cv); Case (RiemannInt_exists 1!([x0:R](Rabsolu (f x0))) 2!a 3!b pr2 5!RinvN RinvN_cv); Intros; Pose phi1 := (phi_sequence RinvN pr1); Pose phi2 := [N:nat](mkStepFun (StepFun_P32 (phi1 N))); Apply Rle_cv_lim with [N:nat](Rabsolu (RiemannInt_SF (phi1 N))) [N:nat](RiemannInt_SF (phi2 N)).
 Intro; Unfold phi2; Apply StepFun_P34; Assumption.
 Fold phi1 in u0; Apply (continuity_seq Rabsolu [N:nat](RiemannInt_SF (phi1 N)) x0); Try Assumption.
 Apply continuity_Rabsolu.
@@ -727,7 +727,7 @@ Elim H0; Clear H0; Intros psi3 H0; Elim H1; Clear H1; Intros psi2 H1; Apply Riem
 Qed.
 
 Lemma RiemannInt_P18 : (f,g:R->R;a,b:R;pr1:(Riemann_integrable f a b);pr2:(Riemann_integrable g a b)) ``a<=b`` -> ((x:R)``a<x<b``->``(f x)==(g x)``) -> ``(RiemannInt pr1)==(RiemannInt pr2)``.
-Intros; Unfold RiemannInt; Case (RiemannInt_exists 1!f 2!a 3!b pr1 5!RinvN RinvN_cv); Case (RiemannInt_exists 1!g 2!a 3!b pr2 5!RinvN RinvN_cv); Intros; EApply UL_sequence.
+Intro f; Intros; Unfold RiemannInt; Case (RiemannInt_exists 1!f 2!a 3!b pr1 5!RinvN RinvN_cv); Case (RiemannInt_exists 1!g 2!a 3!b pr2 5!RinvN RinvN_cv); Intros; EApply UL_sequence.
 Apply u0.
 Pose phi1 := [N:nat](phi_sequence RinvN 2!f 3!a 4!b pr1 N); Change (Un_cv [N:nat](RiemannInt_SF (phi1 N)) x); Assert H1 : (EXT psi1:nat->(StepFun a b) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((f t)-((phi1 n) t)))<= (psi1 n t)``)/\``(Rabsolu (RiemannInt_SF (psi1 n))) < (RinvN n)``).
 Split with [n:nat](projT1 ? ? (phi_sequence_prop RinvN pr1 n)); Intro; Apply (projT2 ? ? (phi_sequence_prop RinvN pr1 n)). 
@@ -803,7 +803,7 @@ Reflexivity.
 Qed.
 
 Lemma RiemannInt_P19 : (f,g:R->R;a,b:R;pr1:(Riemann_integrable f a b);pr2:(Riemann_integrable g a b)) ``a<=b`` -> ((x:R)``a<x<b``->``(f x)<=(g x)``) -> ``(RiemannInt pr1)<=(RiemannInt pr2)``.
-Intros; Apply Rle_anti_compatibility with ``-(RiemannInt pr1)``; Rewrite Rplus_Ropp_l; Rewrite Rplus_sym; Apply Rle_trans with (Rabsolu (RiemannInt (RiemannInt_P10 ``-1`` pr2 pr1))).
+Intro f; Intros; Apply Rle_anti_compatibility with ``-(RiemannInt pr1)``; Rewrite Rplus_Ropp_l; Rewrite Rplus_sym; Apply Rle_trans with (Rabsolu (RiemannInt (RiemannInt_P10 ``-1`` pr2 pr1))).
 Apply Rabsolu_pos.
 Replace ``(RiemannInt pr2)+ -(RiemannInt pr1)`` with (RiemannInt (RiemannInt_P16 (RiemannInt_P10 ``-1`` pr2 pr1))).
 Apply (RiemannInt_P17 (RiemannInt_P10 ``-1`` pr2 pr1) (RiemannInt_P16 (RiemannInt_P10 ``-1`` pr2 pr1))); Assumption.
@@ -1262,7 +1262,7 @@ Rewrite (RiemannInt_P8 pr1 (RiemannInt_P1 pr1)); Rewrite (RiemannInt_P8 pr2 (Rie
 Qed.
 
 Lemma RiemannInt_P27 : (f:R->R;a,b,x:R;h:``a<=b``;C0:((x:R)``a<=x<=b``->(continuity_pt f x))) ``a<x<b`` -> (derivable_pt_lim (primitive h (FTC_P1 h C0)) x (f x)).
-Intros; Elim H; Clear H; Intros; Assert H1 : (continuity_pt f x).
+Intro f; Intros; Elim H; Clear H; Intros; Assert H1 : (continuity_pt f x).
 Apply C0; Split; Left; Assumption.
 Unfold derivable_pt_lim; Intros; Assert Hyp : ``0<eps/2``.
 Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0].
@@ -1392,7 +1392,7 @@ Apply Rle_trans with (Rabsolu h0); [Rewrite <- Rabsolu_Ropp; Apply Rle_Rabsolu |
 Qed.
 
 Lemma RiemannInt_P28 : (f:R->R;a,b,x:R;h:``a<=b``;C0:((x:R)``a<=x<=b``->(continuity_pt f x))) ``a<=x<=b`` -> (derivable_pt_lim (primitive h (FTC_P1 h C0)) x (f x)).
-Intros; Elim h; Intro.
+Intro f; Intros; Elim h; Intro.
 Elim H; Clear H; Intros; Elim H; Intro.
 Elim H1; Intro.
 Apply RiemannInt_P27; Split; Assumption.
@@ -1671,7 +1671,7 @@ Elim n0; Rewrite <- H0; Left; Assumption.
 Qed.
 
 Lemma RiemannInt_P29 : (f:R->R;a,b;h:``a<=b``;C0:((x:R)``a<=x<=b``->(continuity_pt f x))) (antiderivative f (primitive h (FTC_P1 h C0)) a b).
-Intros; Unfold antiderivative; Split; Try Assumption; Intros; Assert H0 := (RiemannInt_P28 h C0 H); Assert H1 : (derivable_pt (primitive h (FTC_P1 h C0)) x); [Unfold derivable_pt; Split with (f x); Apply H0 | Split with H1; Symmetry; Apply derive_pt_eq_0; Apply H0].
+Intro f; Intros; Unfold antiderivative; Split; Try Assumption; Intros; Assert H0 := (RiemannInt_P28 h C0 H); Assert H1 : (derivable_pt (primitive h (FTC_P1 h C0)) x); [Unfold derivable_pt; Split with (f x); Apply H0 | Split with H1; Symmetry; Apply derive_pt_eq_0; Apply H0].
 Qed.
 
 Lemma RiemannInt_P30 : (f:R->R;a,b:R) ``a<=b`` -> ((x:R)``a<=x<=b``->(continuity_pt f x)) -> (sigTT ? [g:R->R](antiderivative f g a b)).
@@ -1684,19 +1684,19 @@ diff0 : (derivable c1);
 cont1 : (continuity (derive c1 diff0)) }.
 
 Lemma RiemannInt_P31 : (f:C1_fun;a,b:R) ``a<=b`` -> (antiderivative (derive f (diff0 f)) f a b).
-Intros; Unfold antiderivative; Split; Try Assumption; Intros; Split with (diff0 f x); Reflexivity.
+Intro f; Intros; Unfold antiderivative; Split; Try Assumption; Intros; Split with (diff0 f x); Reflexivity.
 Qed.
 
 Lemma RiemannInt_P32 : (f:C1_fun;a,b:R) (Riemann_integrable (derive f (diff0 f)) a b).
-Intros; Case (total_order_Rle a b); Intro; [Apply continuity_implies_RiemannInt; Try Assumption; Intros; Apply (cont1 f) | Assert H : ``b<=a``; [Auto with real | Apply RiemannInt_P1; Apply continuity_implies_RiemannInt; Try Assumption; Intros; Apply (cont1 f)]].
+Intro f; Intros; Case (total_order_Rle a b); Intro; [Apply continuity_implies_RiemannInt; Try Assumption; Intros; Apply (cont1 f) | Assert H : ``b<=a``; [Auto with real | Apply RiemannInt_P1; Apply continuity_implies_RiemannInt; Try Assumption; Intros; Apply (cont1 f)]].
 Qed.
 
 Lemma RiemannInt_P33 : (f:C1_fun;a,b:R;pr:(Riemann_integrable (derive f (diff0 f)) a b)) ``a<=b`` -> (RiemannInt pr)==``(f b)-(f a)``.
-Intros; Assert H0 : (x:R)``a<=x<=b``->(continuity_pt (derive f (diff0 f)) x).
+Intro f; Intros; Assert H0 : (x:R)``a<=x<=b``->(continuity_pt (derive f (diff0 f)) x).
 Intros; Apply (cont1 f).
 Rewrite (RiemannInt_P20 H (FTC_P1 H H0) pr); Assert H1 := (RiemannInt_P29 H H0); Assert H2 := (RiemannInt_P31 f H); Elim (antiderivative_Ucte (derive f (diff0 f)) ? ? ? ? H1 H2); Intros C H3; Repeat Rewrite H3; [Ring | Split; [Right; Reflexivity | Assumption] | Split; [Assumption | Right; Reflexivity]].
 Qed.
 
 Lemma FTC_Riemann : (f:C1_fun;a,b:R;pr:(Riemann_integrable (derive f (diff0 f)) a b)) (RiemannInt pr)==``(f b)-(f a)``.
-Intros; Case (total_order_Rle a b); Intro; [Apply RiemannInt_P33; Assumption | Assert H : ``b<=a``; [Auto with real | Assert H0 := (RiemannInt_P1 pr); Rewrite (RiemannInt_P8 pr H0); Rewrite (RiemannInt_P33 H0 H); Ring]].
+Intro f; Intros; Case (total_order_Rle a b); Intro; [Apply RiemannInt_P33; Assumption | Assert H : ``b<=a``; [Auto with real | Assert H0 := (RiemannInt_P1 pr); Rewrite (RiemannInt_P8 pr H0); Rewrite (RiemannInt_P33 H0 H); Ring]].
 Qed.
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index 3681dd3931..8c1329e4ed 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -27,7 +27,7 @@ Unfold INZ;Intros; Apply inject_nat_complete_inf; Assumption.
 Qed.
 
 Lemma Nzorn : (I:nat->Prop) (EX n:nat | (I n)) -> (Nbound I) -> (sigTT ?  [n:nat](I n)/\(i:nat)(I i)->(le i n)).
-Intros; Pose E := [x:R](EX i:nat | (I i)/\(INR i)==x); Assert H1 : (bound E).
+Intros I H H0; Pose E := [x:R](EX i:nat | (I i)/\(INR i)==x); Assert H1 : (bound E).
 Unfold Nbound in H0; Elim H0; Intros N H1; Unfold bound; Exists (INR N); Unfold is_upper_bound; Intros; Unfold E in H2; Elim H2; Intros; Elim H3; Intros; Rewrite <- H5; Apply le_INR; Apply H1; Assumption.
 Assert H2 : (EXT x:R | (E x)).
 Elim H; Intros; Exists (INR x); Unfold E; Exists x; Split; [Assumption | Reflexivity].
@@ -109,7 +109,7 @@ end.
 (********************************)
 
 Lemma StepFun_P1 : (a,b:R;f:(StepFun a b)) (adapted_couple f a b (subdivision f) (subdivision_val f)).
-Intros; Unfold subdivision_val; Case (projT2 Rlist ([l:Rlist](is_subdivision f a b l)) (pre f)); Intros; Apply a0.
+Intros a b f; Unfold subdivision_val; Case (projT2 Rlist ([l:Rlist](is_subdivision f a b l)) (pre f)); Intros; Apply a0.
 Qed.
 
 Lemma StepFun_P2 : (a,b:R;f:R->R;l,lf:Rlist) (adapted_couple f a b l lf) -> (adapted_couple f b a l lf).
@@ -516,7 +516,7 @@ Intros; Induction l1; [Simpl; Ring | Induction l1; Simpl; [Ring | Simpl in Hrecl
 Qed.
 
 Lemma StepFun_P20 : (l:Rlist;f:R->R) (lt O (Rlength l)) -> (Rlength l)=(S (Rlength (FF l f))).
-Induction l; Intros; [Elim (lt_n_n ? H) | Simpl; Rewrite RList_P18; Rewrite RList_P14; Induction r0; [Reflexivity | Rewrite (H f); [Reflexivity | Simpl; Apply lt_O_Sn]]].
+Intros l f H; NewInduction l; [Elim (lt_n_n ? H) | Simpl; Rewrite RList_P18; Rewrite RList_P14; Reflexivity].
 Qed.
 
 Lemma StepFun_P21 : (a,b:R;f:R->R;l:Rlist) (is_subdivision f a b l) -> (adapted_couple f a b l (FF l f)).
@@ -765,11 +765,11 @@ Clear b0; Apply RList_P17; Try Assumption; [Apply RList_P2; Assumption | Elim (R
 Qed.
 
 Lemma StepFun_P25 : (a,b:R;f,g:R->R;lf,lg:Rlist) (is_subdivision f a b lf) -> (is_subdivision g a b lg) -> (is_subdivision g a b (cons_ORlist lf lg)).
-Intros; Case (total_order_Rle a b); Intro; [Apply StepFun_P24 with f; Assumption | Apply StepFun_P5; Apply StepFun_P24 with f; [Auto with real | Apply StepFun_P5; Assumption | Apply StepFun_P5; Assumption]].
+Intros a b f g lf lg H H0; Case (total_order_Rle a b); Intro; [Apply StepFun_P24 with f; Assumption | Apply StepFun_P5; Apply StepFun_P24 with f; [Auto with real | Apply StepFun_P5; Assumption | Apply StepFun_P5; Assumption]].
 Qed.
 
 Lemma StepFun_P26 : (a,b,l:R;f,g:R->R;l1:Rlist) (is_subdivision f a b l1) -> (is_subdivision g a b l1) -> (is_subdivision [x:R]``(f x)+l*(g x)`` a b l1).
-Unfold is_subdivision; Intros; Elim X; Elim X0; Intros; Clear X X0; Unfold adapted_couple in p p0; Decompose [and] p; Decompose [and] p0; Clear p p0; Apply existTT with (FF l1 [x:R]``(f x)+l*(g x)``); Unfold adapted_couple; Repeat Split; Try Assumption.
+Intros a b l f g l1; Unfold is_subdivision; Intros; Elim X; Elim X0; Intros; Clear X X0; Unfold adapted_couple in p p0; Decompose [and] p; Decompose [and] p0; Clear p p0; Apply existTT with (FF l1 [x:R]``(f x)+l*(g x)``); Unfold adapted_couple; Repeat Split; Try Assumption.
 Apply StepFun_P20; Apply neq_O_lt; Red; Intro; Rewrite <- H8 in H7; Discriminate.
 Intros; Unfold constant_D_eq open_interval; Unfold constant_D_eq open_interval in H9 H4; Intros; Rewrite (H9 ? H8 ? H10); Rewrite (H4 ? H8 ? H10); Assert H11 : ~l1==nil.
 Red; Intro; Rewrite H11 in H8; Elim (lt_n_O ? H8).
@@ -781,20 +781,20 @@ Rewrite RList_P14; Simpl; Rewrite H12 in H8; Simpl in H8; Apply lt_n_S; Apply H8
 Qed.
 
 Lemma StepFun_P27 : (a,b,l:R;f,g:R->R;lf,lg:Rlist) (is_subdivision f a b lf) -> (is_subdivision g a b lg) -> (is_subdivision [x:R]``(f x)+l*(g x)`` a b (cons_ORlist lf lg)).
-Intros; Apply StepFun_P26; [Apply StepFun_P23 with g; Assumption | Apply StepFun_P25 with f; Assumption].
+Intros a b l f g lf lg H H0; Apply StepFun_P26; [Apply StepFun_P23 with g; Assumption | Apply StepFun_P25 with f; Assumption].
 Qed.
 
 (* The set of step functions on [a,b] is a vectorial space *)
 Lemma StepFun_P28 : (a,b,l:R;f,g:(StepFun a b)) (IsStepFun [x:R]``(f x)+l*(g x)`` a b).
-Intros; Unfold IsStepFun; Assert H := (pre f); Assert H0 := (pre g); Unfold IsStepFun in H H0; Elim H; Elim H0; Intros; Apply Specif.existT with (cons_ORlist x0 x); Apply StepFun_P27; Assumption.
+Intros a b l f g; Unfold IsStepFun; Assert H := (pre f); Assert H0 := (pre g); Unfold IsStepFun in H H0; Elim H; Elim H0; Intros; Apply Specif.existT with (cons_ORlist x0 x); Apply StepFun_P27; Assumption.
 Qed.
 
 Lemma StepFun_P29 : (a,b:R;f:(StepFun a b)) (is_subdivision f a b (subdivision f)).
-Intros; Unfold is_subdivision; Apply existTT with (subdivision_val f); Apply StepFun_P1.
+Intros a b f; Unfold is_subdivision; Apply existTT with (subdivision_val f); Apply StepFun_P1.
 Qed.
 
 Lemma StepFun_P30 : (a,b,l:R;f,g:(StepFun a b)) ``(RiemannInt_SF (mkStepFun (StepFun_P28 l f g)))==(RiemannInt_SF f)+l*(RiemannInt_SF g)``.
-Intros; Unfold RiemannInt_SF; Case (total_order_Rle a b); (Intro; Replace ``(Int_SF (subdivision_val (mkStepFun (StepFun_P28 l f g))) (subdivision (mkStepFun (StepFun_P28 l f g))))`` with (Int_SF (FF (cons_ORlist (subdivision f) (subdivision g)) [x:R]``(f x)+l*(g x)``) (cons_ORlist (subdivision f) (subdivision g))); [Rewrite StepFun_P19; Replace (Int_SF (FF (cons_ORlist (subdivision f) (subdivision g)) f) (cons_ORlist (subdivision f) (subdivision g))) with (Int_SF (subdivision_val f) (subdivision f)); [Replace (Int_SF (FF (cons_ORlist (subdivision f) (subdivision g)) g) (cons_ORlist (subdivision f) (subdivision g))) with (Int_SF (subdivision_val g) (subdivision g)); [Ring | Apply StepFun_P17 with (fe g) a b; [Apply StepFun_P1 | Apply StepFun_P21; Apply StepFun_P25 with (fe f); Apply StepFun_P29]] | Apply StepFun_P17 with (fe f) a b; [Apply StepFun_P1 | Apply StepFun_P21; Apply StepFun_P23 with (fe g); Apply StepFun_P29]] | Apply StepFun_P17 with [x:R]``(f x)+l*(g x)`` a b; [Apply StepFun_P21; Apply StepFun_P27; Apply StepFun_P29 | Apply (StepFun_P1 (mkStepFun (StepFun_P28 l f g)))]]).
+Intros a b l f g; Unfold RiemannInt_SF; Case (total_order_Rle a b); (Intro; Replace ``(Int_SF (subdivision_val (mkStepFun (StepFun_P28 l f g))) (subdivision (mkStepFun (StepFun_P28 l f g))))`` with (Int_SF (FF (cons_ORlist (subdivision f) (subdivision g)) [x:R]``(f x)+l*(g x)``) (cons_ORlist (subdivision f) (subdivision g))); [Rewrite StepFun_P19; Replace (Int_SF (FF (cons_ORlist (subdivision f) (subdivision g)) f) (cons_ORlist (subdivision f) (subdivision g))) with (Int_SF (subdivision_val f) (subdivision f)); [Replace (Int_SF (FF (cons_ORlist (subdivision f) (subdivision g)) g) (cons_ORlist (subdivision f) (subdivision g))) with (Int_SF (subdivision_val g) (subdivision g)); [Ring | Apply StepFun_P17 with (fe g) a b; [Apply StepFun_P1 | Apply StepFun_P21; Apply StepFun_P25 with (fe f); Apply StepFun_P29]] | Apply StepFun_P17 with (fe f) a b; [Apply StepFun_P1 | Apply StepFun_P21; Apply StepFun_P23 with (fe g); Apply StepFun_P29]] | Apply StepFun_P17 with [x:R]``(f x)+l*(g x)`` a b; [Apply StepFun_P21; Apply StepFun_P27; Apply StepFun_P29 | Apply (StepFun_P1 (mkStepFun (StepFun_P28 l f g)))]]).
 Qed.
 
 Lemma StepFun_P31 : (a,b:R;f:R->R;l,lf:Rlist) (adapted_couple f a b l lf) -> (adapted_couple [x:R](Rabsolu (f x)) a b l (app_Rlist lf Rabsolu)).
@@ -804,7 +804,7 @@ Intros; Unfold constant_D_eq open_interval; Unfold constant_D_eq open_interval i
 Qed.
 
 Lemma StepFun_P32 : (a,b:R;f:(StepFun a b)) (IsStepFun [x:R](Rabsolu (f x)) a b).
-Intros; Unfold IsStepFun; Apply Specif.existT with (subdivision f); Unfold is_subdivision; Apply existTT with (app_Rlist (subdivision_val f) Rabsolu); Apply StepFun_P31; Apply StepFun_P1.
+Intros a b f; Unfold IsStepFun; Apply Specif.existT with (subdivision f); Unfold is_subdivision; Apply existTT with (app_Rlist (subdivision_val f) Rabsolu); Apply StepFun_P31; Apply StepFun_P1.
 Qed.
 
 Lemma StepFun_P33 : (l2,l1:Rlist) (ordered_Rlist l1) -> ``(Rabsolu (Int_SF l2 l1))<=(Int_SF (app_Rlist l2 Rabsolu) l1)``.
@@ -900,21 +900,21 @@ EApply StepFun_P23; Apply StepFun_P29.
 Qed.
 
 Lemma StepFun_P38 : (l:Rlist;a,b:R;f:R->R) (ordered_Rlist l) -> (pos_Rl l O)==a -> (pos_Rl l (pred (Rlength l)))==b -> (sigTT ? [g:(StepFun a b)](g b)==(f b)/\(i:nat)(lt i (pred (Rlength l)))->(constant_D_eq g (co_interval (pos_Rl l i) (pos_Rl l (S i))) (f (pos_Rl l i)))).
-Induction l.
-Intros; Simpl in H0; Simpl in H1; Exists (mkStepFun (StepFun_P4 a b (f b))); Split.
+Intros l a b f; Generalize a; Clear a; NewInduction l. 
+Intros a H H0 H1; Simpl in H0; Simpl in H1; Exists (mkStepFun (StepFun_P4 a b (f b))); Split.
 Reflexivity.
 Intros; Elim (lt_n_O ? H2).
-Induction r0.
-Intros; Simpl in H1; Simpl in H0; Exists (mkStepFun (StepFun_P4 a b (f b))); Split.
+Intros; NewDestruct l as [|r1 l].
+Simpl in H1; Simpl in H0; Exists (mkStepFun (StepFun_P4 a b (f b))); Split.
 Reflexivity.
-Intros; Elim (lt_n_O ? H2).
-Intros; Clear X; Assert H2 : (ordered_Rlist (cons r1 r2)).
+Intros i H2; Elim (lt_n_O ? H2).
+Intros; Assert H2 : (ordered_Rlist (cons r1 l)).
 Apply RList_P4 with r; Assumption.
-Assert H3 : (pos_Rl (cons r1 r2) O)==r1.
+Assert H3 : (pos_Rl (cons r1 l) O)==r1.
 Reflexivity.
-Assert H4 : (pos_Rl (cons r1 r2) (pred (Rlength (cons r1 r2))))==b.
+Assert H4 : (pos_Rl (cons r1 l) (pred (Rlength (cons r1 l))))==b.
 Rewrite <- H1; Reflexivity.
-Elim (X0 r1 b f H2 H3 H4); Intros g [H5 H6].
+Elim (IHl r1 H2 H3 H4); Intros g [H5 H6].
 Pose g' := [x:R]Cases (total_order_Rle r1 x) of
                       | (leftT _) => (g x)
                       | (rightT _) => (f a) end.
@@ -944,7 +944,7 @@ Simpl; Rewrite H13; Reflexivity.
 Intros; Simpl in H9; Induction i.
 Unfold constant_D_eq open_interval; Simpl; Intros; Assert H16 : (Rmin r1 b)==r1.
 Unfold Rmin; Case (total_order_Rle r1 b); Intro; [Reflexivity | Elim n; Assumption].
-Rewrite H16 in H12; Rewrite H12 in H14; Elim H14; Clear H14; Intros _ H14; Unfold g'; Case (total_order_Rle r1 x); Intro.
+Rewrite H16 in H12; Rewrite H12 in H14; Elim H14; Clear H14; Intros _ H14; Unfold g'; Case (total_order_Rle r1 x); Intro r3.
 Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? r3 H14)).
 Reflexivity.
 Change (constant_D_eq g' (open_interval (pos_Rl lg i) (pos_Rl lg (S i))) (pos_Rl lg2 i)); Clear Hreci; Assert H16 := (H15 i); Assert H17 : (lt i (pred (Rlength lg))).
@@ -968,14 +968,14 @@ Simpl; Unfold g'; Case (total_order_Rle r1 b); Intro.
 Assumption.
 Elim n; Assumption.
 Intros; Simpl in H9; Induction i.
-Unfold constant_D_eq co_interval; Simpl; Intros; Simpl in H0; Rewrite H0; Elim H10; Clear H10; Intros; Unfold g'; Case (total_order_Rle r1 x); Intro.
+Unfold constant_D_eq co_interval; Simpl; Intros; Simpl in H0; Rewrite H0; Elim H10; Clear H10; Intros; Unfold g'; Case (total_order_Rle r1 x); Intro r3.
 Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? r3 H11)).
 Reflexivity.
-Clear Hreci; Change (constant_D_eq (mkStepFun H8) (co_interval (pos_Rl (cons r1 r2) i) (pos_Rl (cons r1 r2) (S i))) (f (pos_Rl (cons r1 r2) i))); Assert H10 := (H6 i); Assert H11 : (lt i (pred (Rlength (cons r1 r2)))).
+Clear Hreci; Change (constant_D_eq (mkStepFun H8) (co_interval (pos_Rl (cons r1 l) i) (pos_Rl (cons r1 l) (S i))) (f (pos_Rl (cons r1 l) i))); Assert H10 := (H6 i); Assert H11 : (lt i (pred (Rlength (cons r1 l)))).
 Simpl; Apply lt_S_n; Assumption.
 Assert H12 := (H10 H11); Unfold constant_D_eq co_interval in H12; Unfold constant_D_eq co_interval; Intros; Rewrite <- (H12 ? H13); Simpl; Unfold g'; Case (total_order_Rle r1 x); Intro.
 Reflexivity.
-Elim n; Elim H13; Clear H13; Intros; Apply Rle_trans with (pos_Rl (cons r1 r2) i); Try Assumption; Change ``(pos_Rl (cons r1 r2) O)<=(pos_Rl (cons r1 r2) i)``; Elim (RList_P6 (cons r1 r2)); Intros; Apply H15; [Assumption | Apply le_O_n | Simpl; Apply lt_trans with (Rlength r2); [Apply lt_S_n; Assumption | Apply lt_n_Sn]].
+Elim n; Elim H13; Clear H13; Intros; Apply Rle_trans with (pos_Rl (cons r1 l) i); Try Assumption; Change ``(pos_Rl (cons r1 l) O)<=(pos_Rl (cons r1 l) i)``; Elim (RList_P6 (cons r1 l)); Intros; Apply H15; [Assumption | Apply le_O_n | Simpl; Apply lt_trans with (Rlength l); [Apply lt_S_n; Assumption | Apply lt_n_Sn]].
 Qed.
 
 Lemma StepFun_P39 : (a,b:R;f:(StepFun a b)) (RiemannInt_SF f)==(Ropp (RiemannInt_SF (mkStepFun (StepFun_P6 (pre f))))).
@@ -987,7 +987,7 @@ Assert H : ``a<b``; [Auto with real | Assert H0 : ``b<a``; [Auto with real | Eli
 Qed.
 
 Lemma StepFun_P40 : (f:R->R;a,b,c:R;l1,l2,lf1,lf2:Rlist) ``a<b`` -> ``b<c`` -> (adapted_couple f a b l1 lf1) -> (adapted_couple f b c l2 lf2) -> (adapted_couple f a c (cons_Rlist l1 l2) (FF (cons_Rlist l1 l2) f)).
-Unfold adapted_couple; Intros; Decompose [and] H1; Decompose [and] H2; Clear H1 H2; Repeat Split.
+Intros f a b c l1 l2 lf1 lf2 H H0 H1 H2; Unfold adapted_couple in H1 H2; Unfold adapted_couple; Decompose [and] H1; Decompose [and] H2; Clear H1 H2; Repeat Split.
 Apply RList_P25; Try Assumption.
 Rewrite H10; Rewrite H4; Unfold Rmin Rmax; Case (total_order_Rle a b); Case (total_order_Rle b c); Intros; (Right; Reflexivity) Orelse (Elim n; Left; Assumption).
 Rewrite RList_P22.
@@ -1117,11 +1117,11 @@ Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H r)).
 Qed.
 
 Lemma StepFun_P42 : (l1,l2:Rlist;f:R->R) (pos_Rl l1 (pred (Rlength l1)))==(pos_Rl l2 O) -> ``(Int_SF (FF (cons_Rlist l1 l2) f) (cons_Rlist l1 l2)) == (Int_SF (FF l1 f) l1) + (Int_SF (FF l2 f) l2)``.
-Induction l1; [Intros; Simpl; Ring | Induction r0; [Intros; Simpl in H0; Simpl; Induction l2; [Simpl; Ring | Simpl; Simpl in H0; Rewrite H0; Ring] | Intros; Simpl; Rewrite Rplus_assoc; Apply Rplus_plus_r; Apply (H0 l2 f); Rewrite <- H1; Reflexivity]].
+Intros l1 l2 f; NewInduction l1 as [|r l1 IHl1]; Intros H; [ Simpl; Ring | NewDestruct l1; [Simpl in H; Simpl; NewDestruct l2; [Simpl; Ring | Simpl; Simpl in H; Rewrite H; Ring] | Simpl; Rewrite Rplus_assoc; Apply Rplus_plus_r; Apply IHl1; Rewrite <- H; Reflexivity]].
 Qed.
 
 Lemma StepFun_P43 : (f:R->R;a,b,c:R;pr1:(IsStepFun f a b);pr2:(IsStepFun f b c);pr3:(IsStepFun f a c)) ``(RiemannInt_SF (mkStepFun pr1))+(RiemannInt_SF (mkStepFun pr2))==(RiemannInt_SF (mkStepFun pr3))``.
-Intros; Assert H1 : (SigT ? [l:Rlist](sigTT ? [l0:Rlist](adapted_couple f a b l l0))).
+Intros f; Intros; Assert H1 : (SigT ? [l:Rlist](sigTT ? [l0:Rlist](adapted_couple f a b l l0))).
 Apply pr1.
 Assert H2 : (SigT ? [l:Rlist](sigTT ? [l0:Rlist](adapted_couple f b c l l0))).
 Apply pr2.
@@ -1260,7 +1260,7 @@ Change (adapted_couple (mkStepFun pr1) a b (subdivision (mkStepFun 1!a 2!b 3!f p
 Qed.
 
 Lemma StepFun_P44 : (f:R->R;a,b,c:R) (IsStepFun f a b) -> ``a<=c<=b`` -> (IsStepFun f a c).
-Intros; Assert H0 : ``a<=b``.
+Intros f; Intros; Assert H0 : ``a<=b``.
 Elim H; Intros; Apply Rle_trans with c; Assumption.
 Elim H; Clear H; Intros; Unfold IsStepFun in X; Unfold is_subdivision in X; Elim X; Clear X; Intros l1 [lf1 H2]; Cut (l1,lf1:Rlist;a,b,c:R;f:R->R) (adapted_couple f a b l1 lf1) -> ``a<=c<=b`` -> (SigT ? [l:Rlist](sigTT ? [l0:Rlist](adapted_couple f a c l l0))).
 Intros; Unfold IsStepFun; Unfold is_subdivision; EApply X.
@@ -1334,7 +1334,7 @@ EApply StepFun_P7; [Elim H0; Intros; Apply Rle_trans with c; [Apply H2 | Apply H
 Qed.
 
 Lemma StepFun_P45 : (f:R->R;a,b,c:R) (IsStepFun f a b) -> ``a<=c<=b`` -> (IsStepFun f c b).
-Intros; Assert H0 : ``a<=b``.
+Intros f; Intros; Assert H0 : ``a<=b``.
 Elim H; Intros; Apply Rle_trans with c; Assumption.
 Elim H; Clear H; Intros; Unfold IsStepFun in X; Unfold is_subdivision in X; Elim X; Clear X; Intros l1 [lf1 H2]; Cut (l1,lf1:Rlist;a,b,c:R;f:R->R) (adapted_couple f a b l1 lf1) -> ``a<=c<=b`` -> (SigT ? [l:Rlist](sigTT ? [l0:Rlist](adapted_couple f c b l l0))).
 Intros; Unfold IsStepFun; Unfold is_subdivision; EApply X; [Apply H2 | Split; Assumption].
@@ -1381,7 +1381,7 @@ EApply StepFun_P7; [Elim H0; Intros; Apply Rle_trans with c; [Apply H2 | Apply H
 Qed.
 
 Lemma StepFun_P46 : (f:R->R;a,b,c:R) (IsStepFun f a b) -> (IsStepFun f b c) -> (IsStepFun f a c).
-Intros; Case (total_order_Rle a b); Case (total_order_Rle b c); Intros.
+Intros f; Intros; Case (total_order_Rle a b); Case (total_order_Rle b c); Intros.
 Apply StepFun_P41 with b; Assumption.
 Case (total_order_Rle a c); Intro.
 Apply StepFun_P44 with b; Try Assumption.