Commit 5d3200bd authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove useless From.

parent 2a719755
......@@ -19,7 +19,7 @@ COPYING file for more details.
(** Translation from Flocq to Pff *)
From Flocq Require Import Pff Core Binary.
Require Import Pff Core Binary.
Section RND_Closest_c.
(* extension of pff for rounding function with arbitrary tie *)
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