From 9219b6cd8d1d189cbd5c3a3ed14af1cfaae5839d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Fri, 29 Jul 2022 15:07:54 +0200
Subject: [PATCH] hint locality

---
 theories/lib/debruijn.v                          |  4 ++--
 .../program_logics/concurrent_logrel/syntactic.v |  8 ++++----
 theories/program_logics/heap_lang/derived_laws.v |  2 +-
 theories/program_logics/hoare.v                  |  2 +-
 theories/program_logics/hoare_lib.v              |  2 +-
 theories/program_logics/ipm.v                    |  3 ++-
 theories/program_logics/later_loeb.v             |  2 +-
 theories/program_logics/logrel/syntactic.v       |  8 ++++----
 .../program_logics/reloc/contextual_refinement.v |  4 ++--
 theories/program_logics/reloc/syntactic.v        |  8 ++++----
 theories/type_systems/stlc/lang.v                |  6 +++---
 theories/type_systems/stlc_extended/lang.v       |  6 +++---
 theories/type_systems/systemf/lang.v             |  8 ++++----
 theories/type_systems/systemf/types.v            |  8 ++++----
 theories/type_systems/systemf_mu/lang.v          |  8 ++++----
 theories/type_systems/systemf_mu/logrel.v        |  6 +++---
 theories/type_systems/systemf_mu/types.v         |  8 ++++----
 theories/type_systems/systemf_mu_state/lang.v    |  8 ++++----
 theories/type_systems/systemf_mu_state/logrel.v  | 16 ++++++++--------
 theories/type_systems/systemf_mu_state/types.v   |  8 ++++----
 20 files changed, 63 insertions(+), 62 deletions(-)

diff --git a/theories/lib/debruijn.v b/theories/lib/debruijn.v
index 885f72f..8561e52 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 f894ba3..71da61e 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 5bf05db..f703761 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 ea272a6..700af14 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 f8f3007..aa20491 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 0c2e784..dd650c2 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 0b5568a..a4e09d1 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 05879a1..6f27dd7 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 9202969..38a8699 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 04ef245..97bbb24 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 ffadbca..b668d78 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 337c77b..b075ae9 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 695af68..fee6a90 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 3377b83..7346fad 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 da4fe4c..b07b847 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 6888c34..0fceaeb 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 e72425a..a8e88e6 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 d9ab665..8f5c3b4 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 8786a2b..fccf98b 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 b5bf5ae..d1f982d 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.
-- 
GitLab