I get compile error on server when I use another file's theorem.

[minsuu]

When I was working on P03.v of assignment 2, I used the previously proven theorem in P01.v. It worked well when I ran make on local environment, however, I got compile error on server like following:

STDERR:
File "./P03.v", line 15, characters 22-37:
Error: The reference P01.*** was not found in the current
environment.
make[1]: *** [P03.vo] Error 1
make: *** [P03.vo] Error 2

I tried many different ways to use the theorem in P01.v, finally I redefined it in P03.v and got it right. What is the problem here? My submission number is 104-106.

[jeehoonkang]

Hi! The behavior of the evaluation server is intended. This is to reject such a case:

// P01.v
Lemma f: False. Proof. FILL_IN_HERE. Qed.

// P03.v
Lemma lemma: L. Proof. exfals. appply f. Qed.

[jeehoonkang]

If you need the same definition several times, please just copy-and-paste it over P??.v files wherever needed. Sorry for the inconvenience.

[minsuu]

Thanks for the reply!