]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/fourierR.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / tactics / fourierR.ml
index 1c4e40ed3601fa3dbeab5d2cf910ebffca3f93d2..13dd9f410af6c74b2019842158a4a1b1a96a25c0 100644 (file)
@@ -692,17 +692,19 @@ let tac_zero_infeq_false gl (n,d) =
   apply_tactic 
    (Tacticals.then_
     ~start:
-      (ReductionTactics.fold_tac ~reduction:CicReduction.whd
+      (ReductionTactics.fold_tac
+        ~reduction:(const_lazy_reduction CicReduction.whd)
         ~pattern:(ProofEngineTypes.conclusion_pattern None)
         ~term:
-          (Cic.Appl
+          (const_lazy_term
+            (Cic.Appl
             [_Rle ; _R0 ;
               Cic.Appl
-               [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]]))
+               [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]])))
     ~continuation:
       (Tacticals.then_ 
         ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
-        ~continuation:(tac_zero_inf_pos (-n,d)))) 
+        ~continuation:(tac_zero_inf_pos (-n,d))))
    status 
  in
   mk_tactic (tac_zero_infeq_false gl (n,d))
@@ -898,7 +900,7 @@ let equality_replace a b =
 
 let tcl_fail a (proof,goal) =
   match a with
-    1 -> raise (ProofEngineTypes.Fail "fail-tactical")
+    1 -> raise (ProofEngineTypes.Fail (lazy "fail-tactical"))
   | _ -> (proof,[goal])
 ;;
 
@@ -915,7 +917,7 @@ let assumption_tac (proof,goal)=
         )  
           context 
   in
-  Tacticals.try_tactics ~tactics:tac_list (proof,goal)
+  Tacticals.first ~tactics:tac_list (proof,goal)
 ;;
 *)
 (* Galla: moved in negationTactics.ml
@@ -1135,7 +1137,7 @@ let rec fourier (s_proof,s_goal)=
              apply_tactic 
               (ReductionTactics.change_tac
                 ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
-                (Cic.Appl [ _not; ineq])) 
+                (const_lazy_term (Cic.Appl [ _not; ineq])))
               status))
            ~continuation:(Tacticals.then_ 
              ~start:(PrimitiveTactics.apply_tac ~term:
@@ -1162,7 +1164,7 @@ let rec fourier (s_proof,s_goal)=
                    r))
                  ~continuations:
                    [PrimitiveTactics.apply_tac ~term:_Rinv_R1;
-                   Tacticals.try_tactics 
+                   Tacticals.first 
                      ~tactics:[ "ring",Ring.ring_tac; "id", Tacticals.id_tac] 
                    ])
                ;(*Tacticals.id_tac*)
@@ -1181,7 +1183,7 @@ let rec fourier (s_proof,s_goal)=
                    let r = apply_tactic 
                    (ReductionTactics.change_tac
                       ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
-                      w1) status
+                      (const_lazy_term w1)) status
                    in
                    debug("fine MY_CHNGE\n");
                    r))