Added new tactics: Exists, Split, Assumption, Absurd, Generalize (doesn't work)

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

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index f6f44e950fe961ce3c7b4f6bb8dd771447b1c1a9..07a94a9b1252108ffed55b294fef0447eab75d3d 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -25,6 +25,7 @@
 
 
 (******************** OTHER USEFUL TACTICS **********************)
+(* Galla: moved in variousTactics.ml
 
 let rewrite_tac ~term:equality ~status:(proof,goal) =
  let module C = Cic in
@@ -85,6 +86,7 @@ let rewrite_simpl_tac ~term ~status =
    (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
   ~status
 ;;
+*)
 
 (******************** THE FOURIER TACTIC ***********************)
 
@@ -966,7 +968,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) =
-    rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
+    VariousTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
      ~status:((curi,metasenv',pbo,pty),goal)
    in
    let new_goals = fresh_meta::goals in
@@ -1002,7 +1004,7 @@ let contradiction_tac ~status:(proof,goal)=
        Tacticals.then_ 
                ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima  della chiamata*)
                ~continuation:(Tacticals.then_ 
-                       ~start:(Ring.elim_type_tac ~term:_False) 
+                       ~start:(VariousTactics.elim_type_tac ~term:_False) 
                        ~continuation:(assumption_tac))
        ~status:(proof,goal) 
 ;;