package rocq-runtime

  1. Overview
  2. Docs

Module IndTyping.NotPrimRecordReasonSource

Sourcetype t =
  1. | MustNotBeSquashed
  2. | MustHaveRelevantProj
  3. | MustHaveProj
  4. | MustNotHaveAnonProj