Make Autosubst-generated instances global.

theories/AutoSubst/Ast.v

@@ -1273,17 +1273,17 @@ Class Up_term X Y :=
 Class Up_sort X Y :=
     up_sort : X -> Y.
 
-Instance Subst_term : (Subst1 _ _ _) := @subst_term.
+#[global]Instance Subst_term : (Subst1 _ _ _) := @subst_term.
 
-Instance Subst_sort : (Subst1 _ _ _) | 2 := @subst_sort.
+#[global]Instance Subst_sort : (Subst1 _ _ _) | 2 := @subst_sort.
 
-Instance Up_term_term : (Up_term _ _) := @up_term_term.
+#[global]Instance Up_term_term : (Up_term _ _) := @up_term_term.
 
-Instance Ren_term : (Ren1 _ _ _) := @ren_term.
+#[global]Instance Ren_term : (Ren1 _ _ _) := @ren_term.
 
-Instance Ren_sort : (Ren1 _ _ _) | 2 := @ren_sort.
+#[global]Instance Ren_sort : (Ren1 _ _ _) | 2 := @ren_sort.
 
-Instance VarInstance_term : (Var _ _) := @tRel.
+#[global]Instance VarInstance_term : (Var _ _) := @tRel.
 
 Notation "[ sigma_term ]" := (subst_term sigma_term)
   ( at level 1, left associativity, only printing) : fscope.
@@ -1332,14 +1332,14 @@ exact (fun f_term g_term Eq_term s t Eq_st =>
          (ext_term f_term g_term Eq_term s) t Eq_st).
 Qed.
 
-Instance subst_term_morphism2 :
+#[global]Instance subst_term_morphism2 :
  (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq))
     (@subst_term)).
 Proof.
 exact (fun f_term g_term Eq_term s => ext_term f_term g_term Eq_term s).
 Qed.
 
-Instance subst_sort_morphism :
+#[global]Instance subst_sort_morphism :
  (Proper (respectful (pointwise_relation _ eq) (respectful eq eq))
     (@subst_sort)).
 Proof.
@@ -1348,14 +1348,14 @@ exact (fun f_term g_term Eq_term s t Eq_st =>
          (ext_sort f_term g_term Eq_term s) t Eq_st).
 Qed.
 
-Instance subst_sort_morphism2 :
+#[global]Instance subst_sort_morphism2 :
  (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq))
     (@subst_sort)).
 Proof.
 exact (fun f_term g_term Eq_term s => ext_sort f_term g_term Eq_term s).
 Qed.
 
-Instance ren_term_morphism :
+#[global]Instance ren_term_morphism :
  (Proper (respectful (pointwise_relation _ eq) (respectful eq eq))
     (@ren_term)).
 Proof.
@@ -1364,14 +1364,14 @@ exact (fun f_term g_term Eq_term s t Eq_st =>
          (extRen_term f_term g_term Eq_term s) t Eq_st).
 Qed.
 
-Instance ren_term_morphism2 :
+#[global]Instance ren_term_morphism2 :
  (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq))
     (@ren_term)).
 Proof.
 exact (fun f_term g_term Eq_term s => extRen_term f_term g_term Eq_term s).
 Qed.
 
-Instance ren_sort_morphism :
+#[global]Instance ren_sort_morphism :
  (Proper (respectful (pointwise_relation _ eq) (respectful eq eq))
     (@ren_sort)).
 Proof.
@@ -1380,7 +1380,7 @@ exact (fun f_term g_term Eq_term s t Eq_st =>
          (extRen_sort f_term g_term Eq_term s) t Eq_st).
 Qed.
 
-Instance ren_sort_morphism2 :
+#[global]Instance ren_sort_morphism2 :
  (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq))
     (@ren_sort)).
 Proof.