I proved some basic properties of fields based on the axioms here, and now I continued to define axioms of vector spaces. In particular, `Field.v`

contains the following lines:

```
(***********)
(* IMPORTS *)
(***********)
Require Import Setoid Morphisms.
Variable (F:Type).
Variable (zero:F).
Variable (one :F).
Variable (add: F -> F -> F).
Variable (mul: F -> F -> F).
Variable (eq: F -> F -> Prop).
```

I imported it in a file called `VectorSpace.v`

but Coq complains it doesn't know of `F`

:

```
(*******************)
(* GENERAL IMPORTS *)
(*******************)
Require Import Setoid Morphisms.
(*******************)
(* PROJECT IMPORTS *)
(*******************)
Require Import Field.
(****************)
(* Vector Space *)
(****************)
Variable (V:Type).
Variable (zerov:V).
Variable (onev :V).
Variable (addv: V -> V -> V).
Variable (mulv: F -> V -> V).
```

Here is the error message:

```
The reference F was not found in the current environment.
```

Replace

`Variable`

by`Axiom`

declarations everywhere.Create a

`_CoqProject`

file at the root of your project with the structure of your project. For instance:Now, you can use

`MyProject.Field`

to refer to`Field.v`

in`VectorSpace.v`

(I believe you were importing the`Field`

module from the standard library before).Generate a makefile and compile the project:

If you are using Proof General in Emacs, it should be possible to run through

`VectorSpace.v`

interactively. I believe that CoqIDE has some support for automating steps (2) and (3), but I am not sure.