- write_tac fixed (the list of new goals was empty)

- some new bugs introduced here and there ;-)

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index c46973e2cbeffab6cffc4a95224136ffb4603d07..566003e8992452771e80daeff7e46e413768170c 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -68,10 +68,15 @@ prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
     let irl =
      ProofEngineHelpers.identity_relocation_list_for_metavariable context in
     let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
-     PrimitiveTactics.exact_tac  
-      (C.Appl
-        [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
-       ((curi,metasenv',pbo,pty),goal)
+    
+     let (proof',goals) =
+      PrimitiveTactics.exact_tac  
+       ~term:(C.Appl 
+         [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
+        ~status:((curi,metasenv',pbo,pty),goal)
+     in
+      assert (List.length goals = 0) ;
+      (proof',[fresh_meta])
 ;;
 
 (******************** THE FOURIER TACTIC ***********************)
@@ -520,7 +525,7 @@ let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_ut
 let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") 0 ;;
 let _Ropp = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;;
 let _Rplus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;;
-let _sym_eqT = Cic.Const(UriManager.uri_of_string "/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;;
+let _sym_eqT = Cic.Const(UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;;
 (*****************************************************************************************************)
 let is_int x = (x.den)=1
 ;;
@@ -1036,21 +1041,27 @@ let rec fourier ~status:(s_proof,s_goal)=
                                                ~term:(if sres then _Rnot_lt_lt else _Rnot_le_le))
                                ~continuation:(Tacticals.thens 
                                                ~start:(equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc)
-                                               ~continuations:[tac2;(Tacticals.thens 
+                                               ~continuations:[(*tac2;*)(Tacticals.thens 
                                                        ~start:(equality_replace (Cic.Appl[_Rinv;_R1]) _R1)
                                                        ~continuations:   
-(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ...   *)
-                                       [Tacticals.try_tactics 
-                                               (* ???????????????????????????? *)
-                                               ~tactics:[ "ring", Ring.ring_tac  ; "id", Ring.id_tac] 
-                                       ;
-                                       Tacticals.then_ 
-                                               ~start:(PrimitiveTactics.apply_tac ~term:_sym_eqT)
-                                               ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1)
-                                       ]
+               [
+               (*
+               Tacticals.try_tactics 
+                       (* ???????????????????????????? *)
+               ~tactics:[ "ring", Ring.ring_tac  ; "id", Ring.id_tac] 
+                               ;*)
+               Tacticals.then_ 
+               ~start:(PrimitiveTactics.apply_tac ~term:_sym_eqT)
+               ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1)
+               ;
+               Tacticals.try_tactics 
+                       (* ???????????????????????????? *)
+               ~tactics:[ "ring", Ring.ring_tac  ; "id", Ring.id_tac] 
+               
+               ]
                                
                                         )
-                                               ] (* end continuations before comment *)
+                                       ;tac2   ] (* end continuations before comment *)
                                        )
                                );
                        !tac1]