[Work and discussion in progress] Add Unguarded syntax for (co)fixpoints and Assumed Positive for (co)inductive types. - #7651

[Work and discussion in progress] Add Unguarded syntax for (co)fixpoints and Assumed Positive for (co)inductive types.#7651

SimonBoulier wants to merge 6 commits into

rocq-prover:masterrocq-prover/rocq:masterfrom

SimonBoulier:unsafe_fixpointsSimonBoulier/coq:unsafe_fixpointsCopy head branch name to clipboard