Skip to content
Fetching contributors…
Cannot retrieve contributors at this time
21 lines (19 sloc) 713 Bytes
#!/bin/bash
# This is a wrapper around coqtop which tricks Coq into using the HoTT
# standard library and enables the HoTT-specific options. One day we
# might figure out how to create an honest Coq toplevel instead.
prefix=@prefix@
COQTOP="@COQTOP@"
# If there is a coq/theories directory in the same directory as this script,
# then use that one, otherwise use the global one. This trick allows hoqtop
# to work "in place" on the source files.
mydir=`dirname $0`
if test -d $mydir/coq/theories
then
COQLIB="$mydir/coq"
HOTTLIB="$mydir/theories"
else
COQLIB="@hottdir@/coq"
HOTTLIB="@hottdir@/theories"
fi
exec $COQTOP -coqlib $COQLIB -R $HOTTLIB HoTT -relevant-equality -warn-universe-inconsistency $@
Something went wrong with that request. Please try again.