Make Permutation_cons and _app' #[export]

Fix coq#15596 (we still get a slowdown on Require Import)
Maybe we should use Hint Extern or just don't declare these Proper
instances instead.

theories/Sorting/Permutation.v

@@ -106,7 +106,7 @@ Proof.
   now apply IHHP; rewrite <- app_assoc.
 Qed.
 
-#[global]
+#[export]
 Instance Permutation_cons A :
  Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A).
 Proof.
@@ -161,7 +161,7 @@ Proof.
   apply Permutation_app_tail; assumption.
 Qed.
 
-Global Instance Permutation_app' :
+#[export] Instance Permutation_app' :
  Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A).
 Proof.
   repeat intro; now apply Permutation_app.