More debug printings.

Replacing the wrong tac with id_tac it goes straight to the end,
lefting 1 more goals open:
0 < (1+0)/(1+0)

Remember that the tactic fails applying
0<1 to 0<1+0

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 5fa37103070316b30b6d96e8980137335bf5e7f8..0998a37d0b1c4139bf5752e118b06c65d5816c49 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -541,7 +541,7 @@ let tac_zero_inf_pos (n,d) ~status =
 
 
 
-debug("\nTAC ZERO INF POS\n");
+debug("TAC ZERO INF POS\n");
 
 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) 
   ~continuations:[
@@ -632,8 +632,13 @@ let my_cut ~term:c ~status:(proof,goal)=
 
 let exact = PrimitiveTactics.exact_tac;;
 
-let tac_use h ~status = 
+let tac_use h ~status:(proof,goal as status) = 
 debug("Inizio TC_USE\n");
+let curi,metasenv,pbo,pty = proof in
+let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+debug ("hname = "^ CicPp.ppterm h.hname ^"\n"); 
+debug ("ty = "^ CicPp.ppterm ty^"\n"); 
+
 let res = 
 match h.htype with
   "Rlt" -> exact ~term:h.hname ~status
@@ -648,7 +653,7 @@ match h.htype with
       ~continuation:(exact ~term:h.hname)) ~status
   |_->assert false
 in
-debug("Fine TAC_USE");
+debug("Fine TAC_USE\n");
 res
 ;;
 
@@ -885,12 +890,27 @@ let rec fourier ~status:(s_proof,s_goal)=
           (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
        
           debug "inizio a costruire tac1\n";
+         Fourier.print_rational(c1);
          
           let tac1=ref ( fun ~status -> 
-                       debug "Sotto tattica t1\n";
+                       debug ("Sotto tattica t1 "^(if h1.hstrict then "strict" else "lasc")^"\n");
                        if h1.hstrict then 
-                           (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_lt)
-                                             ~continuations:[tac_use h1;tac_zero_inf_pos (rational_to_fraction c1)] ~status)
+                           (Tacticals.thens ~start:(
+                           fun ~status -> 
+                           debug ("inizio t1 strict\n");
+                           let curi,metasenv,pbo,pty = proof in
+                           let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+                           debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); 
+                           debug ("ty = "^ CicPp.ppterm ty^"\n"); 
+     
+                           PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
+                                             ~continuations:[tac_use h1;
+                                            
+                                               Ring.id_tac] ~status
+                                            
+                                            (*tac_zero_inf_pos (rational_to_fraction c1)] ~status*)
+                                            
+                                            )
                          else 
                            (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
                                              ~continuations:[tac_use h1;tac_zero_inf_pos                                                 (rational_to_fraction c1)] ~status))
@@ -903,18 +923,33 @@ let rec fourier ~status:(s_proof,s_goal)=
                    (if h.hstrict then 
                        (debug("tac1 1\n");
                        tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac 
-                                                      ~term:_Rfourier_lt_lt)
+                                                       ~term:_Rfourier_lt_lt)
                                               ~continuations:[!tac1;tac_use h;
                                                       tac_zero_inf_pos   
                                                       (rational_to_fraction c)]))
                    else 
                    (
                        debug("tac1 2\n");
-                       tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac 
-                                                      ~term:_Rfourier_lt_le)
+                       Fourier.print_rational(c1);
+                       tac1:=(Tacticals.thens ~start:(
+                                       fun ~status -> 
+                                       debug("INIZIO TAC 1 2\n");
+                                       
+                                       let curi,metasenv,pbo,pty = proof in
+                                       let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+                                       debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n"); 
+                                       debug ("ty = "^ CicPp.ppterm ty^"\n"); 
+     
+                                       PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status
+                                                      
+                                                      )
                                               ~continuations:[!tac1;tac_use h; 
-                                                      tac_zero_inf_pos  
-                                                       (rational_to_fraction c)]))
+                                                      
+                                                      Ring.id_tac
+                                                      (*tac_zero_inf_pos  
+                                                       (rational_to_fraction c)*)
+                                                      
+                                                      ]))
                     )
                else 
                    (if h.hstrict then