The Coq mailing list

[t x <txrev319 AT gmail.com>]

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!