Then you have to patch your logic and make sure that none of your proofs relied on that inconsistency. Or something like that.
Each of these constructors takes a natural number as an argument.
It then defines a function `is_256` which checks whether it's argument has the form `C_256 n` for some `n`, returning a boolean.
It then defines the value `falso` of type `False` (which shouldn't be possible). It does this by defining two values: one has type `is_256 (C_256 0) = true`, the other has type `is_256 (C_256 0) = false`. This is clearly a contradiction, which is used to construct the value `falso`.
The reason one value gives `true` and the other `false` is that the former is getting calculated by the regular Coq implementation, whilst the latter is getting calculated by the buggy `vm_compute` alternative. vm_compute should give identical results, but faster; but since there's a bug, we can derive a contradiction by mixing correctly-calculated values with incorrectly-calculated values.
EDIT: For example: 1+1=3. That's false. We've learnt that false=true, therefore 1+1=3 is true.