Newbie problem in CoqIDE on windows

Hi all,
I am an absolute newbie to Coq; I have just downloaded and and run the installer for windows. I plan to use the built-in GAPPA functionality in order to obtain and compare error bounds for floating-point calculations that can be formulated in several mathematically equivalent ways.
Unfortunately, the error message
“Unable to locate library Fcore.”
pops up when I try to execute the following example, the first lines of which I have compiled from the GAPPA manual:
Require Import Reals.
Require Import Fcore.
Require Import Gappa_tactic.
Open Scope R_scope.
@rnd = float< ieee_64, ne >;
xsq = xx*xx;
xsqrnd = rnd(xsq);
omxsq = 1-xsq;
omxsqrnd = rnd(1-xsqrnd);
sqrtomxsq = sqrt(omxsq);
sqrtomxsqrnd = rnd(sqrtomxsq);
errout = (sqrtomxsqrnd - sqrtomxsq);
{ xx in [0,1] -> |errout| in ? };
Importing “Reals” works, but importing “Fcore” does not.
What am I missing? I checked every box I could find in during installation.
I have already replaced “V8.9.1” by “current” in the two hardcoded path entries for refman and stdlib, resp., in the file coqiderc found in $home\AppData\Local\coq. The help now works, but “Fcore” still is not found.

All the best


It may be the case that gappa’s manual is a bit outdated. Ping @silene.

If in your preamble, you instead write:

From Coq Require Import Reals.
From Flocq Require Import Core.
From Gappa Require Import Gappa_tactic.
Open Scope R_scope.

then you can run the examples from the “Coq and Gappa” chapter of the manual.

Tested with Coq 8.9.1, Flocq 3.1.0, gappalib 1.4.1 and gappa 1.3.5.

Thank you very much for your detailed hints, Vincent!
From browsing the Coq library I meanwhile had concluded that the second and third modules mentioned in the script do not exist (anymore).
I will soon try out your preamble and the examples you pointed me to.