The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

If you google "private inductive types coq", you get things like https://coq.inria.fr/files/coq5-slides-bertot.pdf, https://coq.inria.fr/files/coq5_submission_3.pdf, and http://www.crm.cat/en/Activities/Documents/barras-crm-2013.pdf, which might be preliminary "documentation"

On Sun, May 29, 2016 at 10:18 AM Jonathan Leivent <jonikelee AT gmail.com> wrote:

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