Skip to content
This repository
Fetching contributors…

Cannot retrieve contributors at this time

file 18 lines (18 sloc) 0.624 kb
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
#!/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 $@
Something went wrong with that request. Please try again.