X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FfourierR.ml;h=bb1c2febf583893ed8c81fe387908782c39b0d3f;hb=7ff85e55518d06d96b9abbea4aa68d83e6be35b0;hp=c08183bebf889300aa8c56893930d4a842e3deaf;hpb=9597e7e79ce0606671f8aa170951d119419780ad;p=helm.git

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index c08183beb..bb1c2febf 100644
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -775,7 +775,8 @@ let r =
      (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
      Tacticals.then_
       ~start:
-        (ReductionTactics.fold_tac ~also_in_hypotheses:false
+        (ReductionTactics.fold_tac ~reduction:CicReduction.whd
+          ~also_in_hypotheses:false
           ~term:
             (Cic.Appl
               [_Rle ; _R0 ;
@@ -1003,8 +1004,7 @@ let assumption_tac ~status:(proof,goal)=
 let contradiction_tac ~status:(proof,goal)=
 	Tacticals.then_ 
                 (*inutile sia questo che quello prima  della chiamata*)
-		~start:
-                  (PrimitiveTactics.intros_tac ~mknames:(function () -> "boh"))
+		~start:PrimitiveTactics.intros_tac
 		~continuation:(Tacticals.then_ 
 			~start:(VariousTactics.elim_type_tac ~term:_False) 
 			~continuation:(assumption_tac))
@@ -1044,11 +1044,11 @@ theoreme,so let's parse our thesis *)
 
    (* now let's change our thesis applying the th and put it with hp *) 
 
-   let proof,gl = Tacticals.then_ 
-   	~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
-	~continuation:
-          (PrimitiveTactics.intros_tac ~mknames:(function () -> fhyp))
-		~status:(s_proof,s_goal) in
+   let proof,gl =
+    Tacticals.then_ 
+     ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
+     ~continuation:PrimitiveTactics.intros_tac
+     ~status:(s_proof,s_goal) in
    let goal = if List.length gl = 1 then List.hd gl 
                                     else failwith "a new goal" in