3 files changed, 5 insertions, 5 deletions
diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
index e893c9f36c..7aa1d0b3e3 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -214,7 +214,7 @@ Tactic Definition ApplyInverse mul FT lvar trm :=
 
 Tactic Definition StrongFail tac := First [tac|Fail 2].
 
-Tactic Definition InverseTestAux FT trm :=
+Recursive Tactic Definition InverseTestAux FT trm :=
   Let AplusT = Eval Cbv Beta Delta [Aplus] Iota in (Aplus FT)
   And AmultT = Eval Cbv Beta Delta [Amult] Iota in (Amult FT)
   And AoppT  = Eval Cbv Beta Delta [Aopp] Iota in (Aopp FT)
@@ -261,7 +261,7 @@ Tactic Definition Reduce FT :=
   Cbv Beta Delta -[AzeroT AoneT AplusT AmultT AoppT AinvT] Zeta Iota
   Orelse Compute.
 
-Tactic Definition Field_Gen_Aux FT :=
+Recursive Tactic Definition Field_Gen_Aux FT :=
   Let AplusT = Eval Cbv Beta Delta [Aplus] Iota in (Aplus FT) In
   Match Context With
   | [|- ?1==?2] ->
diff --git a/theories/Reals/SplitAbsolu.v b/theories/Reals/SplitAbsolu.v
index e904c238d5..bc876692d7 100644
--- a/theories/Reals/SplitAbsolu.v
+++ b/theories/Reals/SplitAbsolu.v
@@ -10,13 +10,13 @@
 
 Require Rbasic_fun.
 
-Tactic Definition SplitAbs :=
+Recursive Tactic Definition SplitAbs :=
   Match Context With
     | [ |- [(case_Rabsolu ?1)] ] -> 
          Case (case_Rabsolu ?1); Try SplitAbs.
 
 
-Tactic Definition SplitAbsolu :=
+Recursive Tactic Definition SplitAbsolu :=
   Match Context With
     | [ id:[(Rabsolu ?)] |- ? ] -> Generalize id; Clear id;Try SplitAbsolu
     | [ |- [(Rabsolu ?1)] ] ->  Unfold Rabsolu; Try SplitAbs;Intros.
diff --git a/theories/Reals/SplitRmult.v b/theories/Reals/SplitRmult.v
index e799c7b8be..71b2ebf215 100644
--- a/theories/Reals/SplitRmult.v
+++ b/theories/Reals/SplitRmult.v
@@ -13,7 +13,7 @@
 
 Require Rbase.
 
-Tactic Definition SplitRmult :=
+Recursive Tactic Definition SplitRmult :=
   Match Context With
   | [ |- ~(Rmult ?1 ?2)==R0 ] -> Apply mult_non_zero; Split;Try SplitRmult.