The user interface for the completeSearchPattern query has been improved.

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

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index f6f44e950fe961ce3c7b4f6bb8dd771447b1c1a9..9076ae70fffce795573bb6733e8140a60e73da04 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 ***********************)
 
@@ -773,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 ;
@@ -966,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) =
-    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
@@ -1000,9 +1003,11 @@ let assumption_tac ~status:(proof,goal)=
 (* !!!!! fix !!!!!!!!!! *)
 let contradiction_tac ~status:(proof,goal)=
        Tacticals.then_ 
-               ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima  della chiamata*)
+                (*inutile sia questo che quello prima  della chiamata*)
+               ~start:
+                  (PrimitiveTactics.intros_tac ~mknames:(function () -> "boh"))
                ~continuation:(Tacticals.then_ 
-                       ~start:(Ring.elim_type_tac ~term:_False) 
+                       ~start:(VariousTactics.elim_type_tac ~term:_False) 
                        ~continuation:(assumption_tac))
        ~status:(proof,goal) 
 ;;
@@ -1042,7 +1047,8 @@ theoreme,so let's parse our thesis *)
 
    let proof,gl = Tacticals.then_ 
        ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
-       ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)
+       ~continuation:
+          (PrimitiveTactics.intros_tac ~mknames:(function () -> fhyp))
                ~status:(s_proof,s_goal) in
    let goal = if List.length gl = 1 then List.hd gl 
                                     else failwith "a new goal" in