The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 05/29/2016 10:11 AM, Jason Gross wrote:
> You can throw it in Prop if you want it to be erased in extraction (and
> then the eliminator also has to target Prop).  I believe the private
> inductive semantics forbid any new pattern matches outside the module.  At
> worst, this will break subject reduction (vm_compute might reject a well
> typed term, unfolding the induction scheme on neutral terms won't work
> nicely), but it won't lead to inconsistency.

Thanks, Jason.  I'll consider trying that.

Is Private documented anywhere?  I can't find any mention of it in the 
refman, and no usage in the standard library.

-- Jonathan