CODEWITHSUNDEEP
coqcoq-tacticcoqide
Sana
Sana

Reputation: 11

Error: Cannot find a physical path bound to logical path Strands. in coq

I have coq file and was working on it for days but now the file giving me following error:

Error: Cannot find a physical path bound to logical path Strands.

also the required packages are as under:

Require Import Lia.
Require Import Coq.Lists.List.
Import Coq.Lists.List.ListNotations.
Require Import Strands.
Require Import Bundles.
Require Import Terms.
Require Import StrandTactics.
Require Import Penetrator.
Require Import MinimalMPT.
Set Implicit Arguments.

I tried changing and removing some packages restart the code but nothing works.

Upvotes: 1

Views: 432

Answers (1)

Yves
Yves

Reputation: 4258

If you go in an empty directory and run the command.

Require Import toto.

You get the error message

Error: Cannot find a physical path bound to logical path toto.

So this is just to say, that you have no compiled file of your development in your current directory with the name Strands.vo

This may be due to the fact that you removed the files (for instance with a make clean command). On my machine, it is usually enough to run make to restore a good state to the current dictory, but I don't know what is your working environment.

Upvotes: 0

Related Questions