[PRL] Need small bit of Coq help.

[Mitchell Wand]

I'm trying to run some Coq code for a paper I'm refereeing.  The beginning
of the file is:

Add LoadPath "tlc/".

Require Import Specif.
Require Import OrderedType OrderedTypeEx.
Require Import Peano_dec.
Require Export LibEnv.
Require Export LibTactics.
Require Export LibVar.

When I run this, I get the message

Error: Cannot find library LibEnv in loadpath

I'm guessing that LibEnv is a library in the directory tlc/ , which the
author did not include in the package.

Is that the likely diagnosis, or is there something I'm missing?

--Mitch
-------------- next part --------------
HTML attachment scrubbed and removed