Example files don't compile if Coquelicot is part of Coq Platform cause of missing logical path for imports
If Coquelicot is installed via opam, e.g. as part of the Coq Platform, the example files like BacS2013.v do not compile because they assume that Coquelicot files are accessible without logical prefix. This makes the first steps with Coquelicot harder because especially new users struggle with supplying -Q and -R options to Coq IDEs.