- idtac used for debugging removed

- bug fixed: the natural number 1 was mapped to (Rplus R1 R0).
  It is now mapped to R1 (as it should be). This close all the
  residual bugs.

Still to do: we need to close the last open branch using equality_replace,
as soon as it is implemented.

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 0998a37d0b1c4139bf5752e118b06c65d5816c49..1de87fdd99c4d6eb53c4185524192c8acd09839e 100644 (file)
--- 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)
                                                       
                                                       ]))
                     )