vrahli/nuprlincoq

Implementation of Nuprl's type theory in Coq

nuprlincoq's Issues

About the copy of intuitionistic nuprl in the "Coq contributions"

Dear @vrahli, @ithaca-markb, @jonsterling, we still have a copy of "intuitionistic-nuprl" in the coq contribs repository. We used to have it for testing but we don't test any more the "contribs" regularly, and, our copy is anyway outdated wrt the current repository. Would it be a problem for you if we remove the outdated coq-contribs copy which is probably causing more confusion than good? For visibility, you could by the way consider joining coq community if you want. Best, @herbelin

Error when running create_makefile.sh

When I run create_makefile.sh on my system (OS X 10.10), I get the following:

coping util/universe-type.v to util/universe.v
coping per/universe2_prop.v to per/universe2.v
coping per/choice-prop.v to per/choice.v
coping per/per_props_more_prop.v to per/per_props_more.v
./create_makefile.sh: line 50: declare: -A: invalid option
declare: usage: declare [-afFirtx] [-p] [name[=value] ...]
./create_makefile.sh: line 126: terms/swap: division by 0 (error token is "p")

-jon

[Question] How to load in proof general?

Do you use Proof General to develop this library? If so, how do I begin editing? When I open bar_induction3.v and try to start interacting, I get the following error:

Error: Cannot find library universe in loadpath