search

SimonBoulier / TypingFlags

A Coq plugin to disable positivity check, guard check and termination check
16 stars 0 forks source link

Make the fact that plugin activates dangerous features obvious when importing it #2

Open anton-trunov opened 6 years ago

anton-trunov commented 6 years ago

Could we import the plugin it as

Require Import TypingFlags.Unsafe.  (* or anything else conveying the same sense *)

instead of the current Require Import TypingFlags.Loader ? [sorry for nitpicking :)]