Skip to Content.
Sympa Menu

coq-club - [Coq-Club] compilation

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] compilation


Chronological Thread 
  • From: Patricia Peratto <psperatto AT vera.com.uy>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] compilation
  • Date: Tue, 22 Sep 2020 15:59:07 -0300 (UYT)
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=psperatto AT vera.com.uy; spf=Pass smtp.mailfrom=psperatto AT vera.com.uy; spf=None smtp.helo=postmaster AT mail.vera.com.uy
  • Dkim-filter: OpenDKIM Filter v2.9.0 mta01.in.vera.com.uy B132D221E2B
  • Ironport-phdr: 9a23:GyCmvhUsVXgOF7Fx+HW7haOMKhXV8LGtZVwlr6E/grcLSJyIuqrYbRWAt8tkgFKBZ4jH8fUM07OQ7/m/HzVcqs/b4DhCKMUKC0Zbz51O3kQJO42sMQXDNvnkbig3ToxpdWRO2DWFC3VTA9v0fFbIo3e/vnY4ExT7MhdpdKyuQtaBx8u42Pqv9JLNfg5GmCSyYa9oLBWxsA7dqtQajZFtJ6osyBbFuGZEdutZyW91O16enAv36sOs8JJ+6ShdtO8t+s9aXanmY6g0SKFTASg7PWwy+MDlrwTIQxGV5nsbXGUWkx5IDBbA4RrnQJr/sTb0u/Rk1iWCMsL4Ub47WTK576d2UxDokzsINyQ48G7MlMN9ir9QrQ+7qBx+x47UZ5yVNOZ7c6jAc94WWXZNU8BMXCNGAo28aJEPAPEAPelFsobyuV0OoxmjCgm2Gejjzj9FimPq0aE/1ekqDAPI0xE6H98WvnrarMv7OqQQXu6ow6bH0TTDb+9N1Djn9ITHbgsure2QUb92bMHfyVMvFwTAjliIs4LqJS+V1v4Ms2eH7upvT/+khXQ5pAFruDev2tssio7UjY8S0lDE7j15z5gvJdKiVE57fdmkHYBOty6ELYt5WNkuTH1vuCY/0LEGpJ66cTEMxZ86xBDfc+SKf5aU7h7/TuqcLit0iGhrdb6inRq+7EmtxvXhWsS2zlpGtDRJn9bWun0DyhDf8MaKRuZ780y82TiP0BrT5fpFIU8piKXUNZghzLwtmZoJqUnNEC/4llv1gqCUa0sr9fSn6+X7Yrj9vJCQK5N7hRriPqgygsCxD+Q2PBYNUWeZ5Oqz26Hs/UzlQLhRlPI6jrXWv4vGKcgHoKOyHhVb3Zw56xmlCjeryNQYkmcDLFJCYB+HipLmO1DKIPziE/ewnU6sny1xy//aOb3hB4/BLmXDkbv5fLZ97VBTyBYrwNxB+55YFqsNLf3vVkPrutHUEwU1PxG1zur/DdVyzIIeWWaBAq+DN6PStEeF5vo0I+mUeoAVoizyK+Q55/7plnI5h0ESfbOz0pcNdH+4GfFmL1+EYXvsmtsBC3sFvhIiTOz2j12PSSJcZ3GrX64l+j47DJ+mApzYS4C2gL2B2T+7EYdMamBHDFCMC3boeJ+eV/cCciLBavNmxzcDTP2qT5IrnUWlsxa/wL56JMLV/DcZvNTtzo4myffUkEQK/CBuDs+c2im1Qnt9gn8PD2sux7hyu0Vh1lCrz6ViirpTEtkV+uIfAVRyDoLV0+EvUoO6YQnGZNrcFQ7+G4n0MXQKVts0huQ2TQNlAdz71ULd0jCjRbQSkvqWFc5sq/+O7z3KP894jk3++uwhgl0hG5sdMGSnguhh+hLaQYXOlgOEhvTyLPVO7Gv27G6GiFG2kgRdWQ90X7/CWClENFXbt92/7UTHCaK/W+0q

I have compiled one file called Ident.v with the following command:

..\bin\coq-makefile -R . .  .\Ident.v -o .\Ident.vos

where Ident.v is the file I want to compile.

It does not give error messages but I can not import it yet.

When I try to open a file with CoqIde gives a compilation error
and I can not open any file.


Regards.
Patricia



Archive powered by MHonArc 2.6.19+.

Top of Page