coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Courtieu <pierre.courtieu AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Coq/CoqIde can't find my first hello world file. Please help!
- Date: Mon, 28 Sep 2015 01:38:19 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-wi0-f169.google.com
- Ironport-phdr: 9a23:bgt8sxBBm/q/k+tgXo+MUyQJP3N1i/DPJgcQr6AfoPdwSP78rsbcNUDSrc9gkEXOFd2CrakU16yL7+u5ATRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/ni6bvp9aKO10ArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIZoGJ/3dKUgTLFeEC9ucyVsvJWq5lH/Sl6k4WJUeWELmFIcCA/cqRr+Q53Zsy3gt+M71jPMbuPsSrVhYTWv9b1mADTvlT0bNjMkuDXPi8Fqlq8dqxW8vQB+zpP8b4ScNf44daTYK4BJDVFdV9pcAnQSSri3aJECWq9YZb5V
Hello, please explain what you typed and where (terminal? inside coqide?) exactly to obtain this error.
Best regards,
Pierre
2015-09-27 2:42 GMT+02:00 Enjoys Math <enjoysmath AT gmail.com>:
Hi :)I saved as MyTutorial1.v. The file is only one line:Check 0.Compilation output:Error: Can't find file C:\MyProjects\Coq\MyTutorial.vI tried it as well from the Coq folder.How can I fix this? Thanks.Regards,-EM
- [Coq-Club] Coq/CoqIde can't find my first hello world file. Please help!, Enjoys Math, 09/27/2015
- Re: [Coq-Club] Coq/CoqIde can't find my first hello world file. Please help!, Pierre Courtieu, 09/28/2015
- Re: [Coq-Club] Coq/CoqIde can't find my first hello world file. Please help!, Laurent Thery, 09/28/2015
Archive powered by MHonArc 2.6.18.