Commit 21b25dff authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu
Browse files

CoercionN is not in scope in TyCoRep

parent d3ce4172
......@@ -889,10 +889,10 @@ role and kind, which is done in the UnivCo constructor.
data UnivCoProvenance
= UnsafeCoerceProv -- ^ From @unsafeCoerce#@. These are unsound.
| PhantomProv CoercionN -- ^ See Note [Phantom coercions]
| PhantomProv Coercion -- ^ See Note [Phantom coercions]
| ProofIrrelProv CoercionN -- ^ From the fact that any two coercions are
-- considered equivalent. See Note [ProofIrrelProv]
| ProofIrrelProv Coercion -- ^ From the fact that any two coercions are
-- considered equivalent. See Note [ProofIrrelProv]
| PluginProv String -- ^ From a plugin, which asserts that this coercion
-- is sound. The string is for the use of the plugin.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment