]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/fourierR.ml
A few other tactics made available to matita.
[helm.git] / helm / ocaml / tactics / fourierR.ml
index 2ee088edbaf551c19239c51a2aab496a6b1dc8c4..724d2c64708d4e4f0a6c2e07d6cf31e49a7224e0 100644 (file)
@@ -693,7 +693,7 @@ let tac_zero_infeq_false gl (n,d) =
    (Tacticals.then_
     ~start:
       (ReductionTactics.fold_tac ~reduction:CicReduction.whd
-        ~also_in_hypotheses:false
+        ~pattern:([],None)
         ~term:
           (Cic.Appl
             [_Rle ; _R0 ;