Commit b401b7c7 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove the old version of the interval tactic.

This commit also removes the interval_intro tactic, which has no
equivalent in the new model.

Tactic options are made a bit more rational along the way.
parent 29a02e9c
This diff is collapsed.
......@@ -46,7 +46,7 @@ Goal
<= 5/65536.
Proof.
intros.
interval with (i_bisect_taylor x 3).
interval with (i_bisect_taylor x, i_degree 3).
Qed.
Goal
......@@ -64,7 +64,7 @@ Goal
Rabs (RInt (fun x => atan (sqrt (x*x + 2)) / (sqrt (x*x + 2) * (x*x + 1))) 0 1
- 5/96*PI*PI) <= 1/1000.
Proof.
interval with (i_integral_prec 9, i_integral_depth 1, i_integral_deg 5).
interval with (i_fuel 2, i_degree 5).
Qed.
Goal
......
......@@ -19,7 +19,7 @@ intros x H.
(*
Time interval with (i_bisect_diff x, i_prec 50, i_depth 16). (* 31 s *)
*)
Time interval with (i_bisect_taylor x 3, i_prec 50). (* 0.48 s *)
Time interval with (i_bisect_taylor x, i_degree 3, i_prec 50). (* 0.48 s *)
Qed.
(* The timings above were obtained using Coq 8.4pl6 *)
......@@ -28,5 +28,5 @@ intros phi Hphi.
(*
Time interval with (i_bisect_diff phi). (* 38 s *)
*)
Time interval with (i_bisect_taylor phi 5). (* 4.4 s *)
Time interval with (i_bisect_taylor phi, i_degree 5). (* 4.4 s *)
Qed.
......@@ -18,5 +18,5 @@ Goal forall x : R, Rabs x <= 35/100 ->
Proof.
intros x Hx p q r.
unfold r, p, q.
interval with (i_prec 40, i_bisect_taylor x 3).
interval with (i_prec 40, i_bisect_taylor x, i_degree 3).
Qed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment