fix: enumeration type noConfusion was not registered

This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.28kernel.29.20function.20expected.20.2EnoConfusion/near/284634050

src/Lean/Meta/Constructions.lean

@@ -114,6 +114,7 @@ where
         hints       := ReducibilityHints.abbrev
       }
       setReducibleAttribute declName
+      modifyEnv fun env => markNoConfusion env declName
 
 def mkNoConfusion (declName : Name) : MetaM Unit := do
   if (← isEnumType declName) then

tests/lean/run/enumNoConfusionIssue.lean

@@ -0,0 +1,13 @@
+inductive MyBool :=
+  | MyTrue
+  | MyFalse
+
+inductive T :=
+  | mk (b: MyBool) (u: Unit)
+
+inductive isTrue: T → Type :=
+  | intro: isTrue (.mk .MyTrue ())
+
+example {τ: T} (h: isTrue τ): Unit :=
+  match τ, h with
+  | .mk .MyTrue (), .intro => ()