Skip to content

Commit 2c46ae4

Browse files
xavierleroyxavierleroy
committed
Qualify Instance and Program Instance as Global
This avoids a new warning of Coq 8.14.
1 parent d687649 commit 2c46ae4

15 files changed

+53
-53
lines changed

‎aarch64/Machregs.v

+2-2
Original file line numberDiff line numberDiff line change
@@ -54,9 +54,9 @@ Proof.
5454
intros. specialize (H r). InvBooleans. auto.
5555
Qed.
5656

57-
Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq.
57+
Global Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq.
5858

59-
Instance Finite_mreg : Finite mreg := {
59+
Global Instance Finite_mreg : Finite mreg := {
6060
Finite_elements := all_mregs;
6161
Finite_elements_spec := all_mregs_complete
6262
}.

‎arm/Machregs.v

+2-2
Original file line numberDiff line numberDiff line change
@@ -57,9 +57,9 @@ Proof.
5757
intros. specialize (H r). InvBooleans. auto.
5858
Qed.
5959

60-
Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq.
60+
Global Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq.
6161

62-
Instance Finite_mreg : Finite mreg := {
62+
Global Instance Finite_mreg : Finite mreg := {
6363
Finite_elements := all_mregs;
6464
Finite_elements_spec := all_mregs_complete
6565
}.

‎backend/Selectionproof.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -1463,7 +1463,7 @@ End PRESERVATION.
14631463

14641464
(** ** Commutation with linking *)
14651465

1466-
Instance TransfSelectionLink : TransfLink match_prog.
1466+
Global Instance TransfSelectionLink : TransfLink match_prog.
14671467
Proof.
14681468
red; intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2].
14691469
eapply link_match_program; eauto.

‎backend/Unusedglobproof.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -1435,4 +1435,4 @@ Proof.
14351435
* intros. apply PTree.elements_keys_norepet.
14361436
Qed.
14371437

1438-
Instance TransfSelectionLink : TransfLink match_prog := link_match_program.
1438+
Global Instance TransfSelectionLink : TransfLink match_prog := link_match_program.

‎cfrontend/Cshmgenproof.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -1968,7 +1968,7 @@ End CORRECTNESS.
19681968

19691969
(** ** Commutation with linking *)
19701970

1971-
Instance TransfCshmgenLink : TransfLink match_prog.
1971+
Global Instance TransfCshmgenLink : TransfLink match_prog.
19721972
Proof.
19731973
red; intros. destruct (link_linkorder _ _ _ H) as (LO1 & LO2).
19741974
generalize H.

‎cfrontend/Ctypes.v

+4-4
Original file line numberDiff line numberDiff line change
@@ -1530,7 +1530,7 @@ Unset Implicit Arguments.
15301530

15311531
(** ** Linking types *)
15321532

1533-
Program Instance Linker_types : Linker type := {
1533+
Global Program Instance Linker_types : Linker type := {
15341534
link := fun t1 t2 => if type_eq t1 t2 then Some t1 else None;
15351535
linkorder := fun t1 t2 => t1 = t2
15361536
}.
@@ -1579,7 +1579,7 @@ Proof.
15791579
assert (x = y) by eauto. subst y. auto.
15801580
Qed.
15811581

1582-
Program Instance Linker_composite_defs : Linker (list composite_definition) := {
1582+
Global Program Instance Linker_composite_defs : Linker (list composite_definition) := {
15831583
link := link_composite_defs;
15841584
linkorder := @List.incl composite_definition
15851585
}.
@@ -1765,7 +1765,7 @@ Inductive linkorder_fundef {F: Type}: fundef F -> fundef F -> Prop :=
17651765
| linkorder_fundef_ext_int: forall f id sg targs tres cc,
17661766
linkorder_fundef (External (EF_external id sg) targs tres cc) (Internal f).
17671767

1768-
Program Instance Linker_fundef (F: Type): Linker (fundef F) := {
1768+
Global Program Instance Linker_fundef (F: Type): Linker (fundef F) := {
17691769
link := link_fundef;
17701770
linkorder := linkorder_fundef
17711771
}.
@@ -1828,7 +1828,7 @@ Definition linkorder_program {F: Type} (p1 p2: program F) : Prop :=
18281828
linkorder (program_of_program p1) (program_of_program p2)
18291829
/\ (forall id co, p1.(prog_comp_env)!id = Some co -> p2.(prog_comp_env)!id = Some co).
18301830

1831-
Program Instance Linker_program (F: Type): Linker (program F) := {
1831+
Global Program Instance Linker_program (F: Type): Linker (program F) := {
18321832
link := link_program;
18331833
linkorder := linkorder_program
18341834
}.

‎cfrontend/SimplExprproof.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -2444,7 +2444,7 @@ End PRESERVATION.
24442444

24452445
(** ** Commutation with linking *)
24462446

2447-
Instance TransfSimplExprLink : TransfLink match_prog.
2447+
Global Instance TransfSimplExprLink : TransfLink match_prog.
24482448
Proof.
24492449
red; intros. eapply Ctypes.link_match_program_gen; eauto.
24502450
- intros.

‎cfrontend/SimplLocalsproof.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -2320,7 +2320,7 @@ End PRESERVATION.
23202320

23212321
(** ** Commutation with linking *)
23222322

2323-
Instance TransfSimplLocalsLink : TransfLink match_prog.
2323+
Global Instance TransfSimplLocalsLink : TransfLink match_prog.
23242324
Proof.
23252325
red; intros. eapply Ctypes.link_match_program; eauto.
23262326
- intros.

‎common/Linking.v

+10-10
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,7 @@ Inductive linkorder_fundef {F: Type}: fundef F -> fundef F -> Prop :=
6060
| linkorder_fundef_refl: forall fd, linkorder_fundef fd fd
6161
| linkorder_fundef_ext_int: forall f id sg, linkorder_fundef (External (EF_external id sg)) (Internal f).
6262

63-
Program Instance Linker_fundef (F: Type): Linker (fundef F) := {
63+
Global Program Instance Linker_fundef (F: Type): Linker (fundef F) := {
6464
link := link_fundef;
6565
linkorder := linkorder_fundef
6666
}.
@@ -114,7 +114,7 @@ Inductive linkorder_varinit: list init_data -> list init_data -> Prop :=
114114
il <> nil -> init_data_list_size il = sz ->
115115
linkorder_varinit (Init_space sz :: nil) il.
116116

117-
Program Instance Linker_varinit : Linker (list init_data) := {
117+
Global Program Instance Linker_varinit : Linker (list init_data) := {
118118
link := link_varinit;
119119
linkorder := linkorder_varinit
120120
}.
@@ -163,7 +163,7 @@ Inductive linkorder_vardef {V: Type} {LV: Linker V}: globvar V -> globvar V -> P
163163
linkorder i1 i2 ->
164164
linkorder_vardef (mkglobvar info1 i1 ro vo) (mkglobvar info2 i2 ro vo).
165165

166-
Program Instance Linker_vardef (V: Type) {LV: Linker V}: Linker (globvar V) := {
166+
Global Program Instance Linker_vardef (V: Type) {LV: Linker V}: Linker (globvar V) := {
167167
link := link_vardef;
168168
linkorder := linkorder_vardef
169169
}.
@@ -189,7 +189,7 @@ Global Opaque Linker_vardef.
189189

190190
(** A trivial linker for the trivial var info [unit]. *)
191191

192-
Program Instance Linker_unit: Linker unit := {
192+
Global Program Instance Linker_unit: Linker unit := {
193193
link := fun x y => Some tt;
194194
linkorder := fun x y => True
195195
}.
@@ -215,7 +215,7 @@ Inductive linkorder_def {F V: Type} {LF: Linker F} {LV: Linker V}: globdef F V -
215215
linkorder v1 v2 ->
216216
linkorder_def (Gvar v1) (Gvar v2).
217217

218-
Program Instance Linker_def (F V: Type) {LF: Linker F} {LV: Linker V}: Linker (globdef F V) := {
218+
Global Program Instance Linker_def (F V: Type) {LF: Linker F} {LV: Linker V}: Linker (globdef F V) := {
219219
link := link_def;
220220
linkorder := linkorder_def
221221
}.
@@ -332,7 +332,7 @@ Qed.
332332

333333
End LINKER_PROG.
334334

335-
Program Instance Linker_prog (F V: Type) {LF: Linker F} {LV: Linker V} : Linker (program F V) := {
335+
Global Program Instance Linker_prog (F V: Type) {LF: Linker F} {LV: Linker V} : Linker (program F V) := {
336336
link := link_prog;
337337
linkorder := fun p1 p2 =>
338338
p1.(prog_main) = p2.(prog_main)
@@ -699,7 +699,7 @@ Local Transparent Linker_fundef.
699699
- destruct (external_function_eq ef1 ef2); inv H. exists (External ef2); split; auto. simpl. rewrite dec_eq_true; auto.
700700
Qed.
701701

702-
Instance TransfPartialContextualLink
702+
Global Instance TransfPartialContextualLink
703703
{A B C V: Type} {LV: Linker V}
704704
(tr_fun: C -> A -> res B)
705705
(ctx_for: program (fundef A) V -> C):
@@ -714,7 +714,7 @@ Proof.
714714
- intros; subst. exists v; auto.
715715
Qed.
716716

717-
Instance TransfPartialLink
717+
Global Instance TransfPartialLink
718718
{A B V: Type} {LV: Linker V}
719719
(tr_fun: A -> res B):
720720
TransfLink (fun (p1: program (fundef A) V) (p2: program (fundef B) V) =>
@@ -728,7 +728,7 @@ Proof.
728728
- intros; subst. exists v; auto.
729729
Qed.
730730

731-
Instance TransfTotallContextualLink
731+
Global Instance TransfTotallContextualLink
732732
{A B C V: Type} {LV: Linker V}
733733
(tr_fun: C -> A -> B)
734734
(ctx_for: program (fundef A) V -> C):
@@ -747,7 +747,7 @@ Proof.
747747
- intros; subst. exists v; auto.
748748
Qed.
749749

750-
Instance TransfTotalLink
750+
Global Instance TransfTotalLink
751751
{A B V: Type} {LV: Linker V}
752752
(tr_fun: A -> B):
753753
TransfLink (fun (p1: program (fundef A) V) (p2: program (fundef B) V) =>

‎driver/Compiler.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -209,7 +209,7 @@ Proof.
209209
intros. unfold match_if, partial_if in *. destruct (flag tt). auto. congruence.
210210
Qed.
211211

212-
Instance TransfIfLink {A: Type} {LA: Linker A}
212+
Global Instance TransfIfLink {A: Type} {LA: Linker A}
213213
(flag: unit -> bool) (transf: A -> A -> Prop) (TL: TransfLink transf)
214214
: TransfLink (match_if flag transf).
215215
Proof.

‎lib/Decidableplus.v

+21-21
Original file line numberDiff line numberDiff line change
@@ -27,14 +27,14 @@ Ltac decide_goal := eapply Decidable_sound; reflexivity.
2727

2828
(** Deciding logical connectives *)
2929

30-
Program Instance Decidable_not (P: Prop) (dP: Decidable P) : Decidable (~ P) := {
30+
Global Program Instance Decidable_not (P: Prop) (dP: Decidable P) : Decidable (~ P) := {
3131
Decidable_witness := negb (@Decidable_witness P dP)
3232
}.
3333
Next Obligation.
3434
rewrite negb_true_iff. split. apply Decidable_complete_alt. apply Decidable_sound_alt.
3535
Qed.
3636

37-
Program Instance Decidable_equiv (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P <-> Q) := {
37+
Global Program Instance Decidable_equiv (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P <-> Q) := {
3838
Decidable_witness := Bool.eqb (@Decidable_witness P dP) (@Decidable_witness Q dQ)
3939
}.
4040
Next Obligation.
@@ -46,21 +46,21 @@ Next Obligation.
4646
eapply Decidable_sound_alt; rewrite H; eapply Decidable_complete_alt; eauto.
4747
Qed.
4848

49-
Program Instance Decidable_and (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P /\ Q) := {
49+
Global Program Instance Decidable_and (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P /\ Q) := {
5050
Decidable_witness := @Decidable_witness P dP && @Decidable_witness Q dQ
5151
}.
5252
Next Obligation.
5353
rewrite andb_true_iff. rewrite ! Decidable_spec. tauto.
5454
Qed.
5555

56-
Program Instance Decidable_or (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P \/ Q) := {
56+
Global Program Instance Decidable_or (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P \/ Q) := {
5757
Decidable_witness := @Decidable_witness P dP || @Decidable_witness Q dQ
5858
}.
5959
Next Obligation.
6060
rewrite orb_true_iff. rewrite ! Decidable_spec. tauto.
6161
Qed.
6262

63-
Program Instance Decidable_implies (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P -> Q) := {
63+
Global Program Instance Decidable_implies (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P -> Q) := {
6464
Decidable_witness := if @Decidable_witness P dP then @Decidable_witness Q dQ else true
6565
}.
6666
Next Obligation.
@@ -79,28 +79,28 @@ Next Obligation.
7979
split; intros. InvBooleans. auto. subst y. apply dec_eq_true.
8080
Qed.
8181

82-
Program Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := {
82+
Global Program Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := {
8383
Decidable_witness := Bool.eqb x y
8484
}.
8585
Next Obligation.
8686
apply eqb_true_iff.
8787
Qed.
8888

89-
Program Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := {
89+
Global Program Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := {
9090
Decidable_witness := Nat.eqb x y
9191
}.
9292
Next Obligation.
9393
apply Nat.eqb_eq.
9494
Qed.
9595

96-
Program Instance Decidable_eq_positive : forall (x y : positive), Decidable (eq x y) := {
96+
Global Program Instance Decidable_eq_positive : forall (x y : positive), Decidable (eq x y) := {
9797
Decidable_witness := Pos.eqb x y
9898
}.
9999
Next Obligation.
100100
apply Pos.eqb_eq.
101101
Qed.
102102

103-
Program Instance Decidable_eq_Z : forall (x y : Z), Decidable (eq x y) := {
103+
Global Program Instance Decidable_eq_Z : forall (x y : Z), Decidable (eq x y) := {
104104
Decidable_witness := Z.eqb x y
105105
}.
106106
Next Obligation.
@@ -109,35 +109,35 @@ Qed.
109109

110110
(** Deciding order on Z *)
111111

112-
Program Instance Decidable_le_Z : forall (x y: Z), Decidable (x <= y) := {
112+
Global Program Instance Decidable_le_Z : forall (x y: Z), Decidable (x <= y) := {
113113
Decidable_witness := Z.leb x y
114114
}.
115115
Next Obligation.
116116
apply Z.leb_le.
117117
Qed.
118118

119-
Program Instance Decidable_lt_Z : forall (x y: Z), Decidable (x < y) := {
119+
Global Program Instance Decidable_lt_Z : forall (x y: Z), Decidable (x < y) := {
120120
Decidable_witness := Z.ltb x y
121121
}.
122122
Next Obligation.
123123
apply Z.ltb_lt.
124124
Qed.
125125

126-
Program Instance Decidable_ge_Z : forall (x y: Z), Decidable (x >= y) := {
126+
Global Program Instance Decidable_ge_Z : forall (x y: Z), Decidable (x >= y) := {
127127
Decidable_witness := Z.geb x y
128128
}.
129129
Next Obligation.
130130
rewrite Z.geb_le. intuition lia.
131131
Qed.
132132

133-
Program Instance Decidable_gt_Z : forall (x y: Z), Decidable (x > y) := {
133+
Global Program Instance Decidable_gt_Z : forall (x y: Z), Decidable (x > y) := {
134134
Decidable_witness := Z.gtb x y
135135
}.
136136
Next Obligation.
137137
rewrite Z.gtb_lt. intuition lia.
138138
Qed.
139139

140-
Program Instance Decidable_divides : forall (x y: Z), Decidable (x | y) := {
140+
Global Program Instance Decidable_divides : forall (x y: Z), Decidable (x | y) := {
141141
Decidable_witness := Z.eqb y ((y / x) * x)%Z
142142
}.
143143
Next Obligation.
@@ -153,7 +153,7 @@ Qed.
153153

154154
(** Deciding properties over lists *)
155155

156-
Program Instance Decidable_forall_in_list :
156+
Global Program Instance Decidable_forall_in_list :
157157
forall (A: Type) (l: list A) (P: A -> Prop) (dP: forall x:A, Decidable (P x)),
158158
Decidable (forall x:A, In x l -> P x) := {
159159
Decidable_witness := List.forallb (fun x => @Decidable_witness (P x) (dP x)) l
@@ -164,7 +164,7 @@ Next Obligation.
164164
- eapply Decidable_complete; eauto.
165165
Qed.
166166

167-
Program Instance Decidable_exists_in_list :
167+
Global Program Instance Decidable_exists_in_list :
168168
forall (A: Type) (l: list A) (P: A -> Prop) (dP: forall x:A, Decidable (P x)),
169169
Decidable (exists x:A, In x l /\ P x) := {
170170
Decidable_witness := List.existsb (fun x => @Decidable_witness (P x) (dP x)) l
@@ -184,7 +184,7 @@ Class Finite (T: Type) := {
184184

185185
(** Deciding forall and exists quantification over finite types. *)
186186

187-
Program Instance Decidable_forall : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (forall x, P x) := {
187+
Global Program Instance Decidable_forall : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (forall x, P x) := {
188188
Decidable_witness := List.forallb (fun x => @Decidable_witness (P x) (dP x)) (@Finite_elements T fT)
189189
}.
190190
Next Obligation.
@@ -193,7 +193,7 @@ Next Obligation.
193193
- eapply Decidable_complete; eauto.
194194
Qed.
195195

196-
Program Instance Decidable_exists : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (exists x, P x) := {
196+
Global Program Instance Decidable_exists : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (exists x, P x) := {
197197
Decidable_witness := List.existsb (fun x => @Decidable_witness (P x) (dP x)) (@Finite_elements T fT)
198198
}.
199199
Next Obligation.
@@ -204,21 +204,21 @@ Qed.
204204

205205
(** Some examples of finite types. *)
206206

207-
Program Instance Finite_bool : Finite bool := {
207+
Global Program Instance Finite_bool : Finite bool := {
208208
Finite_elements := false :: true :: nil
209209
}.
210210
Next Obligation.
211211
destruct x; auto.
212212
Qed.
213213

214-
Program Instance Finite_pair : forall (A B: Type) (fA: Finite A) (fB: Finite B), Finite (A * B) := {
214+
Global Program Instance Finite_pair : forall (A B: Type) (fA: Finite A) (fB: Finite B), Finite (A * B) := {
215215
Finite_elements := list_prod (@Finite_elements A fA) (@Finite_elements B fB)
216216
}.
217217
Next Obligation.
218218
apply List.in_prod; eapply Finite_elements_spec.
219219
Qed.
220220

221-
Program Instance Finite_option : forall (A: Type) (fA: Finite A), Finite (option A) := {
221+
Global Program Instance Finite_option : forall (A: Type) (fA: Finite A), Finite (option A) := {
222222
Finite_elements := None :: List.map (@Some A) (@Finite_elements A fA)
223223
}.
224224
Next Obligation.

‎lib/Maps.v

+2-2
Original file line numberDiff line numberDiff line change
@@ -1604,7 +1604,7 @@ Proof.
16041604
intros. transitivity a0; auto.
16051605
Qed.
16061606

1607-
Instance Equal_Equivalence : Equivalence Equal := {
1607+
Global Instance Equal_Equivalence : Equivalence Equal := {
16081608
Equivalence_Reflexive := Equal_refl;
16091609
Equivalence_Symmetric := Equal_sym;
16101610
Equivalence_Transitive := Equal_trans
@@ -1633,7 +1633,7 @@ Next Obligation.
16331633
unfold equiv, complement in H0. congruence.
16341634
Qed.
16351635

1636-
Instance Equal_EqDec : EqDec (T.t A) Equal := Equal_dec.
1636+
Global Instance Equal_EqDec : EqDec (T.t A) Equal := Equal_dec.
16371637

16381638
End EXTENSIONAL_EQUALITY.
16391639

0 commit comments

Comments
 (0)