make local instances explicit

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
 

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'.
 

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.