diff --git a/theories/lib/debruijn.v b/theories/lib/debruijn.v
index 885f72f55282a50f7f6e12183c266d53a44fb34f..8561e52a088b2d2d39dd37acca77feb3c5314ffd 100644
--- a/theories/lib/debruijn.v
+++ b/theories/lib/debruijn.v
@@ -33,8 +33,8 @@ Qed.
   [ Definition idsc (n : nat) (sigma : var → var) (x : var) := if decide (x < n) then x else sigma (x - n). ]
   we declare suitable instances to use [idss] for variable renamings.
 *)
-Instance Ids_var : Ids var. exact id. Defined.
-Instance Rename_var : Rename var. exact id. Defined.
+#[global] Instance Ids_var : Ids var. exact id. Defined.
+#[global] Instance Rename_var : Rename var. exact id. Defined.
 
 (* a lemma for the nat instance *)
 Lemma upren_idss sigma n :
diff --git a/theories/program_logics/concurrent_logrel/syntactic.v b/theories/program_logics/concurrent_logrel/syntactic.v
index f894ba3d584e82c85c0f6ea00cc240f4cecd1ae6..71da61e049d02a31ba13cbf42774bc7ddbb00fae 100644
--- a/theories/program_logics/concurrent_logrel/syntactic.v
+++ b/theories/program_logics/concurrent_logrel/syntactic.v
@@ -32,10 +32,10 @@ Implicit Types
 (** Autosubst instances.
   This lets Autosubst do its magic and derive all the substitution functions, etc.
  *)
-Instance Ids_type : Ids type. derive. Defined.
-Instance Rename_type : Rename type. derive. Defined.
-Instance Subst_type : Subst type. derive. Defined.
-Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
+#[export] Instance Ids_type : Ids type. derive. Defined.
+#[export] Instance Rename_type : Rename type. derive. Defined.
+#[export] Instance Subst_type : Subst type. derive. Defined.
+#[export] Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
 
 Declare Scope FType_scope.
 Delimit Scope FType_scope with ty.
diff --git a/theories/program_logics/heap_lang/derived_laws.v b/theories/program_logics/heap_lang/derived_laws.v
index 5bf05db5f3614486c3555818c496c55d3ef3b719..f7037610faf8c384886460bab7c06e0a62a846a9 100644
--- a/theories/program_logics/heap_lang/derived_laws.v
+++ b/theories/program_logics/heap_lang/derived_laws.v
@@ -169,4 +169,4 @@ Qed.
 
 End lifting.
 
-Typeclasses Opaque array.
+#[global] Typeclasses Opaque array.
diff --git a/theories/program_logics/hoare.v b/theories/program_logics/hoare.v
index ea272a69007c680dea56b7b3e1de01243490cd3d..700af1430cc34e5982aaa1d09fa471e66f2b5931 100644
--- a/theories/program_logics/hoare.v
+++ b/theories/program_logics/hoare.v
@@ -529,7 +529,7 @@ Proof.
 Qed.
 
 (* Enables rewriting with equivalences ⊣⊢ in pre/post condition *)
-Instance hoare_proper :
+#[export] Instance hoare_proper :
   Proper (equiv ==> eq ==> (pointwise_relation val (⊢)) ==> impl) hoare.
 Proof.
   intros P1 P2 HP%ent_equiv e1 e2 <- Φ1 Φ2 HΦ Hp.
diff --git a/theories/program_logics/hoare_lib.v b/theories/program_logics/hoare_lib.v
index f8f3007cb19f56bb6f3c5fd32b0dcd1ffddfed6b..aa204910e376d7092aa2f4ddce2f44a824e493ac 100644
--- a/theories/program_logics/hoare_lib.v
+++ b/theories/program_logics/hoare_lib.v
@@ -10,7 +10,7 @@ Module hoare.
   (* We make "ghost_state" an axiom for now to simplify the Coq development.
    In the future, we will quantify over it. *)
   Axiom ghost_state: heapGS heapΣ.
-  Existing Instance ghost_state.
+  #[export] Existing Instance ghost_state.
 
   (* the type of preconditions and postconditions *)
   Notation iProp := (iProp heapΣ).
diff --git a/theories/program_logics/ipm.v b/theories/program_logics/ipm.v
index 0c2e784687fb637458d0863a1f2b14dee798189e..dd650c2ce3527d7c871043cdb009f87f8bda3047 100644
--- a/theories/program_logics/ipm.v
+++ b/theories/program_logics/ipm.v
@@ -300,7 +300,8 @@ Proof.
   iApply ent_wp_pure_step; first done. by iApply "IH".
 Qed.
 
-Print hoare.
+(*Print hoare.*)
+
 (** We can re-derive the Hoare rules from the weakest pre rules. *)
 Lemma hoare_frame' P R Φ e :
   {{ P }} e {{ Φ }} →
diff --git a/theories/program_logics/later_loeb.v b/theories/program_logics/later_loeb.v
index 0b5568a92f7864c3640034582bf049264e8bf450..a4e09d142816c1e3fa9873cf64f824b32910b281 100644
--- a/theories/program_logics/later_loeb.v
+++ b/theories/program_logics/later_loeb.v
@@ -196,7 +196,7 @@ Definition infinite_exec_pre (inf : exprO -n> iPropO) : exprO -n> iPropO :=
   This ensures that we can take the fixpoint.
    (For contractive definitions, Banach's fixpoint theorem ensures that there is a unique fixpoint).
 *)
-Instance infinite_exec_contractive : Contractive (infinite_exec_pre).
+#[local] Instance infinite_exec_contractive : Contractive (infinite_exec_pre).
 Proof. solve_contractive. Qed.
 Definition infinite_exec := fixpoint infinite_exec_pre.
 
diff --git a/theories/program_logics/logrel/syntactic.v b/theories/program_logics/logrel/syntactic.v
index 05879a1485f8c8ee55fe02d4065e1252af6d51d0..6f27dd760a7b4f1c6dcf987183b41d294693dbc5 100644
--- a/theories/program_logics/logrel/syntactic.v
+++ b/theories/program_logics/logrel/syntactic.v
@@ -32,10 +32,10 @@ Implicit Types
 (** Autosubst instances.
   This lets Autosubst do its magic and derive all the substitution functions, etc.
  *)
-Instance Ids_type : Ids type. derive. Defined.
-Instance Rename_type : Rename type. derive. Defined.
-Instance Subst_type : Subst type. derive. Defined.
-Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
+#[export] Instance Ids_type : Ids type. derive. Defined.
+#[export] Instance Rename_type : Rename type. derive. Defined.
+#[export] Instance Subst_type : Subst type. derive. Defined.
+#[export] Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
 
 Declare Scope FType_scope.
 Delimit Scope FType_scope with ty.
diff --git a/theories/program_logics/reloc/contextual_refinement.v b/theories/program_logics/reloc/contextual_refinement.v
index 920296969f7bb0c80cf3c5281a65029b2ee5ea33..38a869922cf182f837451df2c48b4fd8de3f085a 100644
--- a/theories/program_logics/reloc/contextual_refinement.v
+++ b/theories/program_logics/reloc/contextual_refinement.v
@@ -217,14 +217,14 @@ Lemma typed_ctx_typed K Δ Γ A Δ' Γ' B e :
   syn_typed Δ Γ e A → typed_ctx K Δ Γ A Δ' Γ' B → syn_typed Δ' Γ' (fill_ctx K e) B.
 Proof. induction 2; simpl; eauto using typed_ctx_item_typed. Qed.
 
-Instance ctx_refines_reflexive Δ Γ A :
+#[export] Instance ctx_refines_reflexive Δ Γ A :
   Reflexive (fun e1 e2 => ctx_refines Δ Γ e1 e2 A).
 Proof.
   intros e K ????? Hty Hst.
   eexists _,_. apply Hst.
 Qed.
 
-Instance ctx_refines_transitive Δ Γ A :
+#[export] Instance ctx_refines_transitive Δ Γ A :
   Transitive (fun e1 e2 => ctx_refines Δ Γ e1 e2 A).
 Proof.
   intros e1 e2 e3 Hctx1 Hctx2 K σ0 σ1 v1 B Hh Hty Hst.
diff --git a/theories/program_logics/reloc/syntactic.v b/theories/program_logics/reloc/syntactic.v
index 04ef245cb8351f21764ef73e9347fbae06f8545d..97bbb242c764431115bdbe758f5b030d269875f8 100644
--- a/theories/program_logics/reloc/syntactic.v
+++ b/theories/program_logics/reloc/syntactic.v
@@ -32,10 +32,10 @@ Implicit Types
 (** Autosubst instances.
   This lets Autosubst do its magic and derive all the substitution functions, etc.
  *)
-Instance Ids_type : Ids type. derive. Defined.
-Instance Rename_type : Rename type. derive. Defined.
-Instance Subst_type : Subst type. derive. Defined.
-Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
+#[export] Instance Ids_type : Ids type. derive. Defined.
+#[export] Instance Rename_type : Rename type. derive. Defined.
+#[export] Instance Subst_type : Subst type. derive. Defined.
+#[export] Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
 
 Declare Scope FType_scope.
 Delimit Scope FType_scope with ty.
diff --git a/theories/type_systems/stlc/lang.v b/theories/type_systems/stlc/lang.v
index ffadbca1451a9b4d52f750b8f2e0fd70b0f61d1a..b668d788e58034e18da0a2fdef66a7f7fdd52993 100644
--- a/theories/type_systems/stlc/lang.v
+++ b/theories/type_systems/stlc/lang.v
@@ -55,7 +55,7 @@ Qed.
    It is defined as:
     [Inj R S f := ∀ x y, S (f x) (f y) → R x y]
 *)
-Instance of_val_inj : Inj (=) (=) of_val.
+#[export] Instance of_val_inj : Inj (=) (=) of_val.
 Proof. by intros ?? Hv; apply (inj Some); rewrite <-!to_of_val, Hv. Qed.
 
 (* A predicate which holds true whenever an
@@ -269,9 +269,9 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
   end.
 
 Notation closed X e := (Is_true (is_closed X e)).
-Instance closed_proof_irrel X e : ProofIrrel (closed X e).
+#[export] Instance closed_proof_irrel X e : ProofIrrel (closed X e).
 Proof. unfold closed. apply _. Qed.
-Instance closed_dec X e : Decision (closed X e).
+#[export] Instance closed_dec X e : Decision (closed X e).
 Proof. unfold closed. apply _. Defined.
 
 Lemma closed_weaken X Y e : closed X e → X ⊆ Y → closed Y e.
diff --git a/theories/type_systems/stlc_extended/lang.v b/theories/type_systems/stlc_extended/lang.v
index 337c77bb63411b7b00614c69d5e35ae846b9a5fb..b075ae92aecb8a9dd7dfc22d563ac2590465a217 100644
--- a/theories/type_systems/stlc_extended/lang.v
+++ b/theories/type_systems/stlc_extended/lang.v
@@ -74,7 +74,7 @@ Proof.
   revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
 Qed.
 
-Instance of_val_inj : Inj (=) (=) of_val.
+#[export] Instance of_val_inj : Inj (=) (=) of_val.
 Proof. by intros ?? Hv; apply (inj Some); rewrite <-!to_of_val, Hv. Qed.
 
 (** structural computational version *)
@@ -226,9 +226,9 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
 
 (** [closed] states closedness as a Coq proposition, through the [Is_true] transformer. *)
 Definition closed (X : list string) (e : expr) : Prop := Is_true (is_closed X e).
-Instance closed_proof_irrel X e : ProofIrrel (closed X e).
+#[export] Instance closed_proof_irrel X e : ProofIrrel (closed X e).
 Proof. unfold closed. apply _. Qed.
-Instance closed_dec X e : Decision (closed X e).
+#[export] Instance closed_dec X e : Decision (closed X e).
 Proof. unfold closed. apply _. Defined.
 
 (** closed expressions *)
diff --git a/theories/type_systems/systemf/lang.v b/theories/type_systems/systemf/lang.v
index 695af6858e6badac209aef5e49d65873bf357d8f..fee6a9092b4bc61708c493a596c86f165988da13 100644
--- a/theories/type_systems/systemf/lang.v
+++ b/theories/type_systems/systemf/lang.v
@@ -91,7 +91,7 @@ Proof.
   revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
 Qed.
 
-Instance of_val_inj : Inj (=) (=) of_val.
+#[export] Instance of_val_inj : Inj (=) (=) of_val.
 Proof. by intros ?? Hv; apply (inj Some); rewrite <-!to_of_val, Hv. Qed.
 
 (** structural computational version *)
@@ -336,9 +336,9 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
 
 (** [closed] states closedness as a Coq proposition, through the [Is_true] transformer. *)
 Definition closed (X : list string) (e : expr) : Prop := Is_true (is_closed X e).
-Instance closed_proof_irrel X e : ProofIrrel (closed X e).
+#[export] Instance closed_proof_irrel X e : ProofIrrel (closed X e).
 Proof. unfold closed. apply _. Qed.
-Instance closed_dec X e : Decision (closed X e).
+#[export] Instance closed_dec X e : Decision (closed X e).
 Proof. unfold closed. apply _. Defined.
 
 (** closed expressions *)
@@ -507,7 +507,7 @@ Proof.
   by eapply (fill_contextual_step (CaseCtx HoleCtx e1 e2)).
 Qed.
 
-#[global]
+#[export]
 Hint Resolve
   contextual_step_app_l contextual_step_app_r contextual_step_binop_l contextual_step_binop_r
   contextual_step_case contextual_step_fst contextual_step_if contextual_step_injl contextual_step_injr
diff --git a/theories/type_systems/systemf/types.v b/theories/type_systems/systemf/types.v
index 3377b839726405be67f6986a0535ecf8f8b7ad1d..7346fad9a44d3faa9b475f5bbe5e6f261d1093dc 100644
--- a/theories/type_systems/systemf/types.v
+++ b/theories/type_systems/systemf/types.v
@@ -22,10 +22,10 @@ Inductive type : Type :=
 (** Autosubst instances.
   This lets Autosubst do its magic and derive all the substitution functions, etc.
  *)
-Instance Ids_type : Ids type. derive. Defined.
-Instance Rename_type : Rename type. derive. Defined.
-Instance Subst_type : Subst type. derive. Defined.
-Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
+#[export] Instance Ids_type : Ids type. derive. Defined.
+#[export] Instance Rename_type : Rename type. derive. Defined.
+#[export] Instance Subst_type : Subst type. derive. Defined.
+#[export] Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
 
 Definition typing_context := gmap string type.
 Implicit Types
diff --git a/theories/type_systems/systemf_mu/lang.v b/theories/type_systems/systemf_mu/lang.v
index da4fe4cefcd3090f025e8c594db265903c2c94fb..b07b84772e38dff017054b23d1fd3fe72ad31a0e 100644
--- a/theories/type_systems/systemf_mu/lang.v
+++ b/theories/type_systems/systemf_mu/lang.v
@@ -98,7 +98,7 @@ Proof.
   revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
 Qed.
 
-Instance of_val_inj : Inj (=) (=) of_val.
+#[export] Instance of_val_inj : Inj (=) (=) of_val.
 Proof. by intros ?? Hv; apply (inj Some); rewrite <-!to_of_val, Hv. Qed.
 
 (** structural computational version *)
@@ -408,9 +408,9 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
 
 (** [closed] states closedness as a Coq proposition, through the [Is_true] transformer. *)
 Definition closed (X : list string) (e : expr) : Prop := Is_true (is_closed X e).
-Instance closed_proof_irrel X e : ProofIrrel (closed X e).
+#[export] Instance closed_proof_irrel X e : ProofIrrel (closed X e).
 Proof. unfold closed. apply _. Qed.
-Instance closed_dec X e : Decision (closed X e).
+#[export] Instance closed_dec X e : Decision (closed X e).
 Proof. unfold closed. apply _. Defined.
 
 (** closed expressions *)
@@ -724,7 +724,7 @@ Lemma contextual_step_unroll e e':
 Proof. by apply (fill_contextual_step [UnrollCtx]). Qed.
 
 
-#[global]
+#[export]
 Hint Resolve
   contextual_step_app_l contextual_step_app_r contextual_step_binop_l contextual_step_binop_r
   contextual_step_case contextual_step_fst contextual_step_if contextual_step_injl contextual_step_injr
diff --git a/theories/type_systems/systemf_mu/logrel.v b/theories/type_systems/systemf_mu/logrel.v
index 6888c34788f10902ad24852c5a4fa4dcdc7951c7..0fceaeb2fc4e6a4b70cbd4c628941415ae3c1790 100644
--- a/theories/type_systems/systemf_mu/logrel.v
+++ b/theories/type_systems/systemf_mu/logrel.v
@@ -69,7 +69,7 @@ Equations type_size (A : type) : nat :=
 (* [ltof A R] defines a well-founded measure on type [A] by using a mapping [R] from [A] to [nat]
   (it lifts the < relation on natural numbers to [A]) *)
 Definition type_lt := ltof type type_size.
-Instance type_lt_wf : WellFounded type_lt.
+#[local] Instance type_lt_wf : WellFounded type_lt.
 Proof. apply well_founded_ltof. Qed.
 
 Inductive type_case : Set :=
@@ -77,11 +77,11 @@ Inductive type_case : Set :=
 Definition type_case_size (c : type_case) : nat :=
   match c with | expr_case => 1 | val_case => 0 end.
 Definition type_case_lt := ltof type_case type_case_size.
-Instance type_case_lt_wf : WellFounded type_case_lt.
+#[local] Instance type_case_lt_wf : WellFounded type_case_lt.
 Proof. apply well_founded_ltof. Qed.
 
 Definition term_rel := Subterm.lexprod nat (type * type_case) lt (Subterm.lexprod type type_case type_lt type_case_lt).
-Instance term_rel_wf : WellFounded term_rel. apply _. Qed.
+#[local] Instance term_rel_wf : WellFounded term_rel. apply _. Qed.
 
 (** *** The logical relation *)
 (** Since the relation is step-indexed now, and the argument that the case for recursive types is well-formed
diff --git a/theories/type_systems/systemf_mu/types.v b/theories/type_systems/systemf_mu/types.v
index e72425a0e43709f5d8755bb99777fa388984503f..a8e88e62a36dc6bbf2a335c6ca35200ed1262d20 100644
--- a/theories/type_systems/systemf_mu/types.v
+++ b/theories/type_systems/systemf_mu/types.v
@@ -24,10 +24,10 @@ Inductive type : Type :=
 (** Autosubst instances.
   This lets Autosubst do its magic and derive all the substitution functions, etc.
  *)
-Instance Ids_type : Ids type. derive. Defined.
-Instance Rename_type : Rename type. derive. Defined.
-Instance Subst_type : Subst type. derive. Defined.
-Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
+#[export] Instance Ids_type : Ids type. derive. Defined.
+#[export] Instance Rename_type : Rename type. derive. Defined.
+#[export] Instance Subst_type : Subst type. derive. Defined.
+#[export] Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
 
 Definition typing_context := gmap string type.
 Implicit Types
diff --git a/theories/type_systems/systemf_mu_state/lang.v b/theories/type_systems/systemf_mu_state/lang.v
index d9ab6652171b3bc8b52c682a479a1a2657140483..8f5c3b4a7609db56218d0b64a6cf9895ce5f3ac5 100644
--- a/theories/type_systems/systemf_mu_state/lang.v
+++ b/theories/type_systems/systemf_mu_state/lang.v
@@ -103,7 +103,7 @@ Proof.
   revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
 Qed.
 
-Instance of_val_inj : Inj (=) (=) of_val.
+#[export] Instance of_val_inj : Inj (=) (=) of_val.
 Proof. by intros ?? Hv; apply (inj Some); rewrite <-!to_of_val, Hv. Qed.
 
 (** structural computational version *)
@@ -496,9 +496,9 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
 
 (** [closed] states closedness as a Coq proposition, through the [Is_true] transformer. *)
 Definition closed (X : list string) (e : expr) : Prop := Is_true (is_closed X e).
-Instance closed_proof_irrel X e : ProofIrrel (closed X e).
+#[export] Instance closed_proof_irrel X e : ProofIrrel (closed X e).
 Proof. unfold closed. apply _. Qed.
-Instance closed_dec X e : Decision (closed X e).
+#[export] Instance closed_dec X e : Decision (closed X e).
 Proof. unfold closed. apply _. Defined.
 
 (** closed expressions *)
@@ -853,7 +853,7 @@ Proof.
 Qed.
 
 
-#[global]
+#[export]
 Hint Resolve
   contextual_step_app_l contextual_step_app_r contextual_step_binop_l contextual_step_binop_r
   contextual_step_case contextual_step_fst contextual_step_if contextual_step_injl contextual_step_injr
diff --git a/theories/type_systems/systemf_mu_state/logrel.v b/theories/type_systems/systemf_mu_state/logrel.v
index 8786a2b02e87cee83b1c2484e77332c5ef3575fd..fccf98b842421525b37da86d50b298472f51eb8c 100644
--- a/theories/type_systems/systemf_mu_state/logrel.v
+++ b/theories/type_systems/systemf_mu_state/logrel.v
@@ -53,10 +53,10 @@ Coercion of_fotype : fotype >-> type.
 (** Autosubst instances.
   This lets Autosubst do its magic and derive all the substitution functions, etc.
  *)
-Instance Ids_type : Ids type. derive. Defined.
-Instance Rename_type : Rename type. derive. Defined.
-Instance Subst_type : Subst type. derive. Defined.
-Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
+#[export] Instance Ids_type : Ids type. derive. Defined.
+#[export] Instance Rename_type : Rename type. derive. Defined.
+#[export] Instance Subst_type : Subst type. derive. Defined.
+#[export] Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
 
 Definition typing_context := gmap string type.
 Implicit Types
@@ -290,7 +290,7 @@ Implicit Types (W : world) (INV : heap_inv).
 (** [W'] extends [W] if [W] is a suffix of [W'] *)
 Definition wext W W' := suffix W W'.
 Notation "W' ⊒ W" := (wext W W') (at level 40).
-Instance wext_preorder : PreOrder wext.
+#[export] Instance wext_preorder : PreOrder wext.
 Proof. apply _. Qed.
 
 (** Satisfaction is defined straightforwardly by recursion.
@@ -459,7 +459,7 @@ Equations type_size (A : type) : nat :=
 (* [ltof A R] defines a well-founded measure on type [A] by using a mapping [R] from [A] to [nat]
   (it lifts the < relation on natural numbers to [A]) *)
 Definition type_lt := ltof type type_size.
-Instance type_lt_wf : WellFounded type_lt.
+#[local] Instance type_lt_wf : WellFounded type_lt.
 Proof. apply well_founded_ltof. Qed.
 
 Inductive type_case : Set :=
@@ -467,11 +467,11 @@ Inductive type_case : Set :=
 Definition type_case_size (c : type_case) : nat :=
   match c with | expr_case => 1 | val_case => 0 end.
 Definition type_case_lt := ltof type_case type_case_size.
-Instance type_case_lt_wf : WellFounded type_case_lt.
+#[local] Instance type_case_lt_wf : WellFounded type_case_lt.
 Proof. apply well_founded_ltof. Qed.
 
 Definition term_rel := Subterm.lexprod nat (type * type_case) lt (Subterm.lexprod type type_case type_lt type_case_lt).
-Instance term_rel_wf : WellFounded term_rel. apply _. Qed.
+#[local] Instance term_rel_wf : WellFounded term_rel. apply _. Qed.
 
 (** *** The logical relation *)
 (** Since the relation is step-indexed now, and the argument that the case for recursive types is well-formed
diff --git a/theories/type_systems/systemf_mu_state/types.v b/theories/type_systems/systemf_mu_state/types.v
index b5bf5aeb529cce1cbd50e4428d59ad6ebf74d220..d1f982df4c8821061888ab16224f2955e1da7110 100644
--- a/theories/type_systems/systemf_mu_state/types.v
+++ b/theories/type_systems/systemf_mu_state/types.v
@@ -25,10 +25,10 @@ Inductive type : Type :=
 (** Autosubst instances.
   This lets Autosubst do its magic and derive all the substitution functions, etc.
  *)
-Instance Ids_type : Ids type. derive. Defined.
-Instance Rename_type : Rename type. derive. Defined.
-Instance Subst_type : Subst type. derive. Defined.
-Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
+#[export] Instance Ids_type : Ids type. derive. Defined.
+#[export] Instance Rename_type : Rename type. derive. Defined.
+#[export] Instance Subst_type : Subst type. derive. Defined.
+#[export] Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
 
 Definition typing_context := gmap string type.
 Definition heap_context := gmap loc type.