Rearranged tactics in VariousTactics into new modules EqualityTactics, EliminationTac...

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

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index bb1c2febf583893ed8c81fe387908782c39b0d3f..4008836fcb655fffaa272e766da77d27c2eb2e0c 100644 (file)
--- 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,7 +999,8 @@ 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_ 
@@ -1010,6 +1011,7 @@ let contradiction_tac ~status:(proof,goal)=
                        ~continuation:(assumption_tac))
        ~status:(proof,goal) 
 ;;
+*)
 
 (* ********************* TATTICA ******************************** *)