X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FfourierR.ml;h=90657b598fbbcaf5576e32e4b423489c143f56a3;hb=e8393183461d4aa2637b250c8e8d5b303a22c675;hp=bdba623190cc8ab47fa6b533f232ff5a26aec7a7;hpb=251e2f428031db12bae815fb56862e3b6384f0f8;p=helm.git

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index bdba62319..90657b598 100644
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -80,7 +80,10 @@ prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
 
 
 let rewrite_simpl_tac ~term ~status =
- Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation:ReductionTactics.simpl_tac ~status
+ Tacticals.then_ ~start:(rewrite_tac ~term)
+  ~continuation:
+   (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
+  ~status
 ;;
 
 (******************** THE FOURIER TACTIC ***********************)
@@ -391,7 +394,7 @@ let ineq1_of_term (h,t) =
                 |_->assert false)(* match u *)
           | Cic.MutInd (u,i,o) ->
               (match UriManager.string_of_uri u with 
-		 "cic:/Coq/Init/Logic_Type/eqT.con" ->  
+		 "cic:/Coq/Init/Logic_Type/eqT.ind" ->  
 		 	   let t0= arg1 in
                            let arg1= arg2 in
                            let arg2= List.hd(List.tl (List.tl next)) in
@@ -714,7 +717,7 @@ let r =
      (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
      Tacticals.then_
       ~start:
-        (ReductionTactics.fold_tac
+        (ReductionTactics.fold_tac ~also_in_hypotheses:false
           ~term:
             (Cic.Appl
               [_Rle ; _R0 ;
@@ -759,6 +762,9 @@ let my_cut ~term:c ~status:(proof,goal)=
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 
+debug("my_cut di "^CicPp.ppterm c^"\n");
+
+
   let fresh_meta = ProofEngineHelpers.new_meta proof in
   let irl =
    ProofEngineHelpers.identity_relocation_list_for_metavariable context in
@@ -920,7 +926,7 @@ let assumption_tac ~status:(proof,goal)=
 (* !!!!! fix !!!!!!!!!! *)
 let contradiction_tac ~status:(proof,goal)=
 	Tacticals.then_ 
-		~start:(PrimitiveTactics.intros_tac ~name:"bo?" )
+		~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima  della chiamata*)
 		~continuation:(Tacticals.then_ 
 			~start:(Ring.elim_type_tac ~term:_False) 
 			~continuation:(assumption_tac))
@@ -1135,7 +1141,7 @@ theoreme,so let's parse our thesis *)
        in
        tac:=(Tacticals.thens 
          ~start:(my_cut ~term:ineq) 
-         ~continuations:[Tacticals.then_  
+         ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)Tacticals.then_  
 	   ~start:(fun ~status:(proof,goal as status) ->
              let curi,metasenv,pbo,pty = proof in
              let metano,context,ty = List.find (function (m,_,_) -> m=goal) 
@@ -1148,6 +1154,7 @@ theoreme,so let's parse our thesis *)
 	     ~continuation:(Tacticals.thens 
 	       ~start:( 
 		 fun ~status ->
+		 debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
 		 let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc 
 		  ~status
 		 in
@@ -1211,12 +1218,13 @@ theoreme,so let's parse our thesis *)
 		  ) 
 		 ~continuation:(*PORTINGTacticals.id_tac*)tac2]))
 	 ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*)
-       tac:=(Tacticals.thens 
+       (*tac:=(Tacticals.thens 
          ~start:(PrimitiveTactics.cut_tac ~term:_False)
 	 ~continuations:[Tacticals.then_ 
 	   ~start:(PrimitiveTactics.intros_tac ~name:"??")
 	   ~continuation:contradiction_tac
-	 ;!tac])
+	 ;!tac])*)
+	 tac:=!tac
 
 
     |_-> assert false)(*match (!lutil) *)