diff --git a/Makefile.coq.local b/Makefile.coq.local
index e623454d6ddb3e74c2742f40f0ff232567ffffce..4c14b573855386cbc97c29936c54a61fbfde3234 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -16,7 +16,7 @@ test: $(TESTFILES:.v=.vo)
 	$(SHOW)"Performing some style checks..."
 	$(HIDE)for FILE in $(VFILES); do \
 	  if ! fgrep -q 'From stdpp Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi ; \
-	  if egrep '^\s*(Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope)\s' "$$FILE"; then echo "ERROR: $$FILE contains unqualified 'Instance'/'Arguments'/'Hint'/'Scope' (see above)."; echo "Please add 'Global' or 'Local' as appropriate."; echo; exit 1; fi \
+	  if egrep '^\s*((Existing\s+|Program\s+)Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope)\b' "$$FILE"; then echo "ERROR: $$FILE contains unqualified 'Instance'/'Arguments'/'Hint'/'Scope' (see above)."; echo "Please add 'Global' or 'Local' as appropriate."; echo; exit 1; fi \
 	done
 .PHONY: test
 
diff --git a/theories/countable.v b/theories/countable.v
index c4481ba495cfb74b57e5d1d9a9d4280866198c44..535d94b2dd6b56b008f8aecd220f2d67aa6f0484 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -97,7 +97,7 @@ Section inj_countable.
   Context `{Countable A, EqDecision B}.
   Context (f : B → A) (g : A → option B) (fg : ∀ x, g (f x) = Some x).
 
-  Program Instance inj_countable : Countable B :=
+  Program Definition inj_countable : Countable B :=
     {| encode y := encode (f y); decode p := x ← decode p; g x |}.
   Next Obligation. intros y; simpl; rewrite decode_encode; eauto. Qed.
 End inj_countable.
@@ -106,7 +106,7 @@ Section inj_countable'.
   Context `{Countable A, EqDecision B}.
   Context (f : B → A) (g : A → B) (fg : ∀ x, g (f x) = x).
 
-  Program Instance inj_countable' : Countable B := inj_countable f (Some ∘ g) _.
+  Program Definition inj_countable' : Countable B := inj_countable f (Some ∘ g) _.
   Next Obligation. intros x. by f_equal/=. Qed.
 End inj_countable'.
 
diff --git a/theories/finite.v b/theories/finite.v
index 0e9e6fbb005c2bd4ec43a63c39ab2ded80c78330..60b3961a2e565a6d34983afe6c98470f74a9acbc 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -204,7 +204,7 @@ Section enc_finite.
   Context (to_nat_c : ∀ x, to_nat x < c).
   Context (to_of_nat : ∀ i, i < c → to_nat (of_nat i) = i).
 
-  Program Instance enc_finite : Finite A := {| enum := of_nat <$> seq 0 c |}.
+  Local Program Instance enc_finite : Finite A := {| enum := of_nat <$> seq 0 c |}.
   Next Obligation.
     apply NoDup_alt. intros i j x. rewrite !list_lookup_fmap. intros Hi Hj.
     destruct (seq _ _ !! i) as [i'|] eqn:Hi',
@@ -224,7 +224,7 @@ Section surjective_finite.
   Context `{Finite A, EqDecision B} (f : A → B).
   Context `{!Surj (=) f}.
 
-  Program Instance surjective_finite: Finite B :=
+  Program Definition surjective_finite: Finite B :=
     {| enum := remove_dups (f <$> enum A) |}.
   Next Obligation. apply NoDup_remove_dups. Qed.
   Next Obligation.
@@ -237,7 +237,7 @@ Section bijective_finite.
   Context `{Finite A, EqDecision B} (f : A → B) (g : B → A).
   Context `{!Inj (=) (=) f, !Cancel (=) f g}.
 
-  Global Instance bijective_finite: Finite B :=
+  Local Instance bijective_finite: Finite B :=
     let _ := cancel_surj (f:=f) (g:=g) in
     surjective_finite f.
 End bijective_finite.