X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FfourierR.ml;h=4008836fcb655fffaa272e766da77d27c2eb2e0c;hb=370f967a478c116fcc85a81c7953363b4351a2e9;hp=9076ae70fffce795573bb6733e8140a60e73da04;hpb=ba712be83ed64a934037e2310aa5bdef25e9d3b9;p=helm.git

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 9076ae70f..4008836fc 100644
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -969,7 +969,7 @@ debug("inizio EQ\n");
    let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
 debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
    let (proof,goals) =
-    VariousTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
+    EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
      ~status:((curi,metasenv',pbo,pty),goal)
    in
    let new_goals = fresh_meta::goals in
@@ -984,7 +984,7 @@ let tcl_fail a ~status:(proof,goal) =
 	|_-> (proof,[goal])
 ;;
 
-
+(* Galla: moved in variousTactics.ml 
 let assumption_tac ~status:(proof,goal)=
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
@@ -999,18 +999,19 @@ let assumption_tac ~status:(proof,goal)=
   in
   Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
 ;;
-
+*)
+(* Galla: moved in negationTactics.ml
 (* !!!!! fix !!!!!!!!!! *)
 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))
 	~status:(proof,goal) 
 ;;
+*)
 
 (* ********************* TATTICA ******************************** *)
 
@@ -1045,11 +1046,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