Merge pull request #2252 from jdchristensen/export-instances

EMSpace: add #[export] to the instances

Author: Alizter

theories/Homotopy/EMSpace.v

@@ -29,27 +29,27 @@ Notation "'K(' G , n )" := (EilenbergMacLane G n).
 Section EilenbergMacLane.
   Context `{Univalence}.
 
-  Instance istrunc_em {G : Group} {n : nat} : IsTrunc n K(G, n).
+  #[export] Instance istrunc_em {G : Group} {n : nat} : IsTrunc n K(G, n).
   Proof.
     destruct n as [|[]]; exact _.
   Defined.
 
   (** This is subsumed by the next result, but Coq doesn't always find the next result when it should. *)
-  Instance isconnected_em {G : Group} (n : nat)
+  #[export] Instance isconnected_em {G : Group} (n : nat)
     : IsConnected n K(G, n.+1).
   Proof.
     induction n; exact _.
   Defined.
 
-  Instance isconnected_em' {G : Group} (n : nat)
+  #[export] Instance isconnected_em' {G : Group} (n : nat)
     : IsConnected n.-1 K(G, n).
   Proof.
     destruct n.
     1: exact (is_minus_one_connected_pointed _).
     apply isconnected_em.
   Defined.
 
-  Instance is0connected_em {G : Group} (n : nat)
+  #[export] Instance is0connected_em {G : Group} (n : nat)
     : IsConnected 0 K(G, n.+1).
   Proof.
     rapply (is0connected_isconnected n.-2).