The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Fri, 18 Mar 2011 14:41:00 +0000,
Peter Aczel 
<petera AT cs.man.ac.uk>
 a écrit :

> Dear coq-club and coqdev members,
…
> 
> Is there a simple way to bypass the standard library??

I am not sure it is what you want, but:

$ coqc --help

Usage: coqc <options> <Coq options> file...

options are:
  -image f  specify an alternative executable for Coq

Coq options are:
  -inputstate f          read state from file f.coq
  -is f                  (idem)
  -nois                  start with an empty state
  -outputstate f         write state in file f.coq
  -compat X.Y            provides compatibility support for Coq version
  X.Y

same things for coqtop and coqide.
I already used the "-nois" option succesfully; never tried the other
options.

With -nois option, you will only have the "Type" "Prop" and "Set"
constants defined at startup (but the predicativity of these sorts is
not changed by this option)
in coqide/coqtop there is a "-impredicative-set" option, but I find
strange I didn't saw it in the options of coqc, so it may not work.
> 
> Any suggestions for how to proceed would be welcome.  I want to have a
> module type/record type/type class for the notion of a logic, relative
> to a sort of the types for
> the free and bound variables of the logic.  This would have Parameter
> declarations for the logical
> operations and rules of inference and proofs of logic theorems and
> then implement different logics
> as instances of the logic module type/record type/type class.
> 
> Best wishes,
> 
> Peter Aczel