Added variousTactic with Constructor, Left, Right, Exists, Reflexivity, Symmetry...

[helm.git] / helm / gTopLevel / fourierR.ml

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index c8c856459d4ebd65d7cdca91af4ae019d0484bd5..247a47248600e87d270f561bb3398d5480c4e20b 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -1048,7 +1048,7 @@ theoreme,so let's parse our thesis *)
          " disequazioni\n");
 
   let res=fourier_lineq (!lineq) in
-  let tac=ref Ring.id_tac in
+  let tac=ref Tacticals.id_tac in
   if res=[] then 
        (print_string "Tactic Fourier fails.\n";flush stdout;
         failwith "fourier_tac fails")
@@ -1234,7 +1234,7 @@ theoreme,so let's parse our thesis *)
                                        let r = Ring.ring_tac  ~status in
                                        debug ("end RING\n");
                                        r)
-                       ; "id", Ring.id_tac] 
+                       ; "id", Tacticals.id_tac] 
                 ])
 (* CSC: NOW THE BUG IS HERE: tac2 DOES NOT WORK ANY MORE *)
               ;tac2]))