coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "盛枫"<fsheng1990 AT 163.com>
- To: "Coq Club"<coq-club AT inria.fr>
- Subject: [Coq-Club] The compile in Coq 8.5beta
- Date: Thu, 26 Mar 2015 19:22:24 +0800
Hello everyone,
I use the latest version of Coq: Coq 8.5beta. When
I compile a file named Util.v, it will yeild the following messages
and files:
Message: "Running: coqc -I "E:\Coq4MDE"
"E:\Coq4MDE\Util.v" 2>&1";
Files:
.Util.aux
Util.glob
Util.v.d
it could not produce the Util.vo. And when I
import the Util in another file, it occurs an error "Error: Cannot find library
Util in loadpath".
- [Coq-Club] The compile in Coq 8.5beta, 盛枫, 03/26/2015
Archive powered by MHonArc 2.6.18.