Deprecate "~=" notation for JMeq in Program.Equality

Because of #16356

Author: SkySkimmer

doc/changelog/11-standard-library/16436-depr-jmed-notation.rst

@@ -0,0 +1,4 @@
+- **Deprecated:**
+  notation ``_ ~= _`` for ``JMeq`` in
+  ``Coq.Program.Equality`` (`#16436
+  <https://github.com/coq/coq/pull/16436>`_, by Gaëtan Gilbert).

theories/Program/Equality.v

@@ -33,7 +33,7 @@ Ltac block_goal := match goal with [ |- ?T ] => change (block T) end.
 Ltac unblock_goal := unfold block in *.
 
 (** Notation for heterogeneous equality. *)
-
+#[deprecated(since="8.17")]
 Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity).
 
 (** Do something on an heterogeneous equality appearing in the context. *)