doc: remove docstring from implicitDefEqProofs (#5751)

this option was added in fb97275dcb to
prepare for #4595, due to boostrapping issues, but #4595 has not landed
yet. This is be very confusing when people discover this option and try
to use it (as I did).

So let's clearly mark this as not yet implemented on `master`, and add
the
docstring only with #4595.

src/Init/MetaTypes.lean

@@ -224,11 +224,7 @@ structure Config where
   -/
   index             : Bool := true
   /--
-  When `true` (default: `true`), `simp` will **not** create a proof for a rewriting rule associated
-  with an `rfl`-theorem.
-  Rewriting rules are provided by users by annotating theorems with the attribute `@[simp]`.
-  If the proof of the theorem is just `rfl` (reflexivity), and `implicitDefEqProofs := true`, `simp`
-  will **not** create a proof term which is an application of the annotated theorem.
+  This option does not have any effect (yet).
   -/
   implicitDefEqProofs : Bool := true
   deriving Inhabited, BEq