X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FfourierR.ml;h=8b910bded8ebabe6c5695016930b4ef4325c721b;hb=ef3f78973c2fa3151c09681bcdb60107cd73c518;hp=5418e114935cc4af1f0742be18cd64634b70ac75;hpb=aa0d60227b785da3355b31519ba11cb4fbd2c925;p=helm.git

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index 5418e1149..8b910bded 100644
--- a/helm/ocaml/tactics/fourierR.ml
+++ b/helm/ocaml/tactics/fourierR.ml
@@ -196,8 +196,8 @@ let rational_of_const = rational_of_term;;
 *)
 let fails f a =
  try
-   let tmp = (f a) in
-   false
+  ignore (f a);
+  false
  with 
    _-> true
  ;;
@@ -662,11 +662,7 @@ let tac_zero_inf_false gl (n,d) =
     apply_tactic (PrimitiveTactics.apply_tac ~term:_Rnot_lt0) status
    else
     apply_tactic (Tacticals.then_ 
-     ~start:( mk_tactic (fun status -> 
-       let (proof, goal) = status in
-       let curi,metasenv,pbo,pty = proof in
-       let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-        apply_tactic (PrimitiveTactics.apply_tac ~term:_Rle_not_lt) status))
+     ~start:(mk_tactic (apply_tactic (PrimitiveTactics.apply_tac ~term:_Rle_not_lt)))
      ~continuation:(tac_zero_infeq_pos gl (-n,d))) 
     status
  in