Commit 7c6c810d authored by Guillaume Melquiond's avatar Guillaume Melquiond

Use native_compute also for the first evaluation of interval_intro.

parent e0be0a0f
......@@ -458,7 +458,11 @@ Ltac do_interval_intro y extend vars prec degree depth fuel native nocheck eval_
| itm_bisect_diff => constr:(eval_bisect_diff_plain prec depth extend hyps prog consts)
| itm_bisect_taylor => constr:(eval_bisect_taylor_plain prec degree depth extend hyps prog consts)
end in
let yi := eval vm_compute in (extend yi) in
let yi :=
match native with
| true => eval native_compute in (extend yi)
| false => eval vm_compute in (extend yi)
end in
instantiate (i := yi)
end ;
do_reduction nocheck native
......
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