TypingFlags

TypingFlags copied to clipboard

Positivity cheking for type constructor applied to itself

2

Hi, I have some troubles to deactivate the positivity checking. When I do: ```coq From TypingFlags Require Import Loader. Unset Guard Checking. Inductive foo : Type := | bar :...

clarus

Could we import the plugin it as ```coq Require Import TypingFlags.Unsafe. (* or anything else conveying the same sense *) ``` instead of the current `Require Import TypingFlags.Loader` ? [sorry...

anton-trunov