[PRL] Need small bit of Coq help.
Mitchell Wand
wand at ccs.neu.edu
Mon Oct 20 22:06:12 EDT 2014
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
More information about the PRL
mailing list