- new CicTextualParser

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

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 670978e5cf124290fd9544b23b22b6e06c77801f..247a47248600e87d270f561bb3398d5480c4e20b 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -78,33 +78,9 @@ prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
       (proof',[fresh_meta])
 ;;
 
-
-
-let simpl_tac ~status:(proof,goal) =
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-
-prerr_endline("simpl_tac su "^CicPp.ppterm ty);
- 
- let new_ty = ProofEngineReduction.simpl context ty in
-
-prerr_endline("ritorna "^CicPp.ppterm new_ty);
-
- let new_metasenv = 
-   List.map
-   (function
-     (n,_,_) when n = metano -> (metano,context,new_ty)
-     | _ as t -> t
-   ) metasenv
- in
- (curi,new_metasenv,pbo,pty), [metano]
-
-;;
-
-let rewrite_simpl_tac ~term ~status =
-
- Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation:simpl_tac ~status
-
+let rewrite_simpl_tac ~term =
+ Tacticals.then_ ~start:(rewrite_tac ~term)
+  ~continuation:ReductionTactics.simpl_tac
 ;;
 
 (******************** THE FOURIER TACTIC ***********************)
@@ -1072,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")
@@ -1258,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]))