Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

19 lines (18 sloc) 0.624 kB
#!/bin/bash
# This is a wrapper around coqtc which tricks Coq into using the HoTT
# standard library and enables the HoTT-specific options.
prefix=@prefix@
COQC="@COQC@"
# 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 hoqc
# to work "in place" on the source files.
mydir=`dirname $0`
if test -d $mydir/coq/theories
then
COQLIB="$mydir/coq"
HOTLIB="$mydir/theories"
else
COQLIB="@hottdir@/coq"
HOTLIB="@hottdir@/theories"
fi
exec $COQC -coqlib $COQLIB -R $HOTLIB HoTT -relevant-equality -warn-universe-inconsistency $@
Jump to Line
Something went wrong with that request. Please try again.