X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FfourierR.ml;h=1de87fdd99c4d6eb53c4185524192c8acd09839e;hb=1d2bd140d14561951f8214edf15abe4f40dcb649;hp=0998a37d0b1c4139bf5752e118b06c65d5816c49;hpb=7607dbbaf3c411a62300da0594c8b078bca091c5;p=helm.git

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 0998a37d0..1de87fdd9 100644
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -483,6 +483,7 @@ let rec rational_to_fraction x= (x.num,x.den)
 let rec int_to_real_aux n =
   match n with
     0 -> _R0 (* o forse R0 + R0 ????? *)
+  | 1 -> _R1
   | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
 ;;	
 	
@@ -906,9 +907,7 @@ let rec fourier ~status:(s_proof,s_goal)=
 			    PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
                                              ~continuations:[tac_use h1;
 					     
-						Ring.id_tac] ~status
-					     
-					     (*tac_zero_inf_pos (rational_to_fraction c1)] ~status*)
+					     tac_zero_inf_pos (rational_to_fraction c1)] ~status
 					     
 					     )
                          else 
@@ -945,9 +944,7 @@ let rec fourier ~status:(s_proof,s_goal)=
 						       )
 					       ~continuations:[!tac1;tac_use h; 
 					               
-						       Ring.id_tac
-						       (*tac_zero_inf_pos  
-                                                       (rational_to_fraction c)*)
+						       tac_zero_inf_pos (rational_to_fraction c)
 						       
 						       ]))
                     )