Commit 0a6d6120 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Adapt to coq/coq#10476.

parent d568ecd2
......@@ -17,7 +17,9 @@ the economic rights, and the successive licensors have only limited
liability. See the COPYING file for more details.
*)
From Coq Require Import Bool Reals List.
From Coq Require Import Bool Reals.
From Flocq Require Import Zaux Raux.
From Coq Require Import List.
From Coquelicot Require Import Coquelicot.
From mathcomp.ssreflect Require Import ssreflect.
......
......@@ -17,8 +17,9 @@ the economic rights, and the successive licensors have only limited
liability. See the COPYING file for more details.
*)
From Coq Require Import Reals List Psatz.
From Coq Require Import Reals Psatz.
From Flocq Require Import Raux.
From Coq Require Import List.
Require Import Xreal.
Require Import Interval.
......
From Coq Require Import Reals ZArith Psatz Fourier_util.
From Flocq Require Import Raux.
From Coquelicot Require Import Coquelicot AutoDerive.
From mathcomp.ssreflect Require Import ssreflect ssrfun ssrbool ssrnat bigop.
......
......@@ -18,6 +18,7 @@ liability. See the COPYING file for more details.
*)
From Coq Require Import Bool Reals Psatz.
From Flocq Require Import Raux.
Require Import Stdlib.
Require Import Xreal.
......
......@@ -18,7 +18,7 @@ liability. See the COPYING file for more details.
*)
From Coq Require Import Reals Psatz.
From Flocq Require Import Digits.
From Flocq Require Import Raux Digits.
Require Import Stdlib.
Require Import Xreal.
......
......@@ -18,7 +18,7 @@ liability. See the COPYING file for more details.
*)
From Coq Require Import Reals Psatz.
From Flocq Require Export Raux.
From Flocq Require Import Raux.
Ltac evar_last :=
match goal with
......
......@@ -256,7 +256,7 @@ Definition opp := map C.opp.
Section PrecIsPropagated.
Variable u : U.
Definition add := map2 (C.add u) id.
Definition add := map2 (C.add u) (fun x => x).
Definition sub := map2 (C.sub u) C.opp.
......@@ -312,7 +312,7 @@ Qed.
Definition deriv_loop := foldri (fun a i s => C.mul u a (C.from_nat i) :: s) [::].
Definition deriv (p : T) := deriv_loop (behead p) 1%N.
Definition deriv (p : T) := deriv_loop (behead p) 1.
Definition grec1 (A : Type) := @grec1up A C.T.
......
......@@ -18,6 +18,7 @@ liability. See the COPYING file for more details.
*)
From Coq Require Import Reals Bool.
From Flocq Require Import Raux.
From mathcomp.ssreflect Require Import ssreflect.
Require Import Stdlib.
......
......@@ -18,6 +18,7 @@ liability. See the COPYING file for more details.
*)
From Coq Require Import Reals.
From Flocq Require Import Raux.
Require Import Stdlib.
Require Import Xreal.
......
......@@ -18,6 +18,7 @@ liability. See the COPYING file for more details.
*)
From Coq Require Import Reals List ZArith Psatz.
From Flocq Require Import Zaux.
From Coquelicot Require Import Coquelicot.
Require Import Stdlib.
......
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