The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

To answer (B), it is sufficient that your OCaml extensions neither add new axioms nor modify the core checker; the bulk of Coq is used to generate terms of the Gallina language, which are then typechecked by the core checker.  If your extensions only make it easier to generate such terms, then, well, you could have generated them by hand anyway, and so you have not made Coq inconsistent.

-Jason

On Saturday, September 14, 2013, t x wrote:

Please ignore last email, by mtac-1.1/examples/htt/prelude.v, clearly this is valid to do.

On Sat, Sep 14, 2013 at 2:35 PM, t x <txrev319 AT gmail.com> wrote:

Hi,

## Background:

I believe the following:

(1) prop_ext + func_ext + law of excluded + Coq = consistent (as by earlier email thread)

(2) mtac + Coq = consistent

(3) ssreflect + Coq = consistent

Now, I believe that it is safe to use (1) + (2) + (3) because -- to the best of my knowledge, (2)/(3) neither (a) add new axioms nor (b) modify the core checker.

## Questions:

(A) is prop_ext + func_ext + law of exluded middle + mtac + ssreflect safe + Coq safe to use?

(B) In general, suppose {my set of axioms} + Coq = safe to use, then is {my set of axioms} + {ocaml extensions that don't add new adioms} + Coq = safe to use?

(formally, X is "safe to use" if (X is inconsistent implies plain Coq is inconsistent)

Thanks!