The Coq mailing list

[Théo Zimmermann <theo AT irif.fr>]

But usually, users working on a Coq project will avoid calling coqc
manually every time. Soon, you will be better off using one of the
solutions proposed here:
https://coq.inria.fr/refman/practical-tools/utilities.html#building-a-coq-project

In particular, using coq_makefile should be preferred to writing one's
own Makefile.

Best,
Théo

Le mar. 22 sept. 2020 à 10:08, Pierre Courtieu
<pierre.courtieu AT gmail.com> a écrit :
>
> You need to compile the first file with coqc and require it from the
> other file. This should explain how to do it:
>
> In short:
> coqc Foo.v
> will produce a Foo.vo file
>
> and then you can use
> Require Foo.
> in the other file. The definitions of foo will be accessible via the
> qualified names: e.g. "Foo.T" "Foo.f" etc.
> You may consider doing
> Require Import Foo.
> if you want to use short names.
>
> https://coq.inria.fr/distrib/current/refman/language/core/modules.html#
> https://coq.inria.fr/tutorial/3-modules
>
> Best,
> Pierre Courtieu
>
> Le mar. 22 sept. 2020 à 08:46, Patricia Peratto
> <psperatto AT vera.com.uy> a écrit :
> >
> > I have defined some proofs in a file .v and I want to import
> > it inside other file.
> >
> > How can I do this?
> >
> > Regards,
> > Patricia