Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

Commit af78e1cd authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Automatically unfold transparent constants.

parent f314e026
Pipeline #251741 passed with stages
in 23 minutes and 26 seconds
......@@ -240,6 +240,15 @@ Ltac reify t l :=
let n := eval lazy in n in
match is_Z_const n with true => constr:(Econst (Int n)) end
end
| _ =>
let rec head t :=
lazymatch t with
| ?f _ => head f
| _ => t
end in
let h := head t in
let t' := eval unfold h in t in
aux t'
| _ =>
let n := list_find t l in
constr:(Evar n)
......
Require Import Reals.
Require Import Interval.Tactic.
From Coq Require Import Reals.
From Interval Require Import Tactic.
Local Open Scope R_scope.
(*
......@@ -23,7 +23,6 @@ Definition arp phi :=
Goal forall phi, 0 <= phi <= max ->
Rabs ((rp phi - arp phi) / rp phi) <= 23/16777216.
Proof.
unfold rp, arp, umf2, a, f, max.
intros phi Hphi.
(*
Time interval with (i_bisect phi, i_autodiff phi). (* 15 s *)
......
Require Import Reals Interval.Tactic.
From Coq Require Import Reals.
From Interval Require Import Tactic.
Open Scope R_scope.
......@@ -17,6 +18,5 @@ Goal forall x : R, Rabs x <= 35/100 ->
Rabs ((r - exp x) / exp x) <= 17 * pow2 (-34).
Proof.
intros x Hx p q r.
unfold r, p, q.
interval with (i_prec 40, i_bisect x, i_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