coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Impredicative [ Set ]

From: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
To: Vladimir Voevodsky <vladimir AT ias.edu>
Cc: gmalecha AT cs.harvard.edu, Coq-Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Impredicative [ Set ]
Date: Sat, 16 Apr 2011 01:09:58 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; b=bYv4S5hV1e14ZYKi69wJEXgeiG/Q5rfVo8Mj5JkSPDQUp2FMK/uuw9bCzs/Co8TCKg tR+RQDEgAB7iBlDBBA3NfNuw0oacTFuO6CRpe9aE3yL5OxIhAnFxuNEtaNkTRt63FOwS P9Hzr2kvko9HIeHCXu4uDILdtz1/BG93tnLKw=

Hi!

When I use proof general,� I usually have a small shell script that looks like that

#!/bin/sh

PWD=`pwd`

make depend

make -q ${1}o || {
�� make -j2 `grep "^${1}o" .depend | sed -e 's/.*://'`
}

COQPROGNAME="coqtop"
COQPROGARGS="\"-I\" \"$PWD/TCB\" \"-I\" \"$PWD/NTCB\""

emacs --eval "(setq coq-prog-name \"$COQPROGNAME\")" \
�--eval "(setq coq-prog-args '($COQPROGARGS))" $1
&& make ${1}o

You can easily add -impredicative-set in the COQPROGARGS list

Cheers

Alexandre

[Coq-Club] Re: [coqdev] messy behavior with universes, (continued)