From 7f0f113b851b1810d0b2628281a99093eb344127 Mon Sep 17 00:00:00 2001 From: Josselin Poiret Date: Fri, 17 Nov 2023 19:00:20 +0100 Subject: [PATCH] Make Autosubst-generated instances global. --- theories/AutoSubst/Ast.v | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/theories/AutoSubst/Ast.v b/theories/AutoSubst/Ast.v index c47e298..4caca09 100644 --- a/theories/AutoSubst/Ast.v +++ b/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.