The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/25/2015 03:05 AM, Stefan Ciobaca wrote:
> The development is here:
>
> https://github.com/clarus/falso
>
>  From the readme:
>
> "This is an implementation in the Coq proof assistant of the Falso proof
> system. It exploits a bug of thevm_compute command when there is a type
> with more than 255 constructors. The vm_computecommand evaluates a term
> efficiently by compilation to a byte-code. This bug concerns all recent
> versions of Coq, including Coq 8.4pl5."
>
> Cheers,
> Stefan Ciobaca

I don't think it is limited to vm_compute.  For instance, I was able to 
do this without vm_compute:

Lemma inconsistency : true = false.
  pose ((@eq_refl bool false<:@eq bool (is_256 (C_256 O)) false)
          :@eq bool (is_256 (C_256 O)) false).
  assumption.
Qed.

This is using 8.5beta.

-- Jonathan