From d68764918c148a5297c8568dedf496813f720271 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 26 Sep 2021 17:32:27 +0200 Subject: Vendored Flocq library: address Coq 8.14 warning --- flocq/IEEE754/Bits.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/flocq/IEEE754/Bits.v b/flocq/IEEE754/Bits.v index 3c19e31b..b38d4900 100644 --- a/flocq/IEEE754/Bits.v +++ b/flocq/IEEE754/Bits.v @@ -181,7 +181,7 @@ cut (x / (2^mw * 2^ew) < 2)%Z. clear ; lia. apply Zdiv_lt_upper_bound. now apply Zmult_lt_0_compat. rewrite <- Zpower_exp ; try ( apply Z.le_ge ; apply Zlt_le_weak ; assumption ). -change 2%Z at 1 with (Zpower 2 1). +change 2%Z with (Zpower 2 1) at 1. rewrite <- Zpower_exp. now rewrite Zplus_comm. discriminate. -- cgit From 2c46ae4bd8f9f49554daa31988fd98793cc5601e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 26 Sep 2021 17:37:52 +0200 Subject: Qualify `Instance` and `Program Instance` as `Global` This avoids a new warning of Coq 8.14. --- aarch64/Machregs.v | 4 ++-- arm/Machregs.v | 4 ++-- backend/Selectionproof.v | 2 +- backend/Unusedglobproof.v | 2 +- cfrontend/Cshmgenproof.v | 2 +- cfrontend/Ctypes.v | 8 ++++---- cfrontend/SimplExprproof.v | 2 +- cfrontend/SimplLocalsproof.v | 2 +- common/Linking.v | 20 ++++++++++---------- driver/Compiler.v | 2 +- lib/Decidableplus.v | 42 +++++++++++++++++++++--------------------- lib/Maps.v | 4 ++-- powerpc/Machregs.v | 4 ++-- riscV/Machregs.v | 4 ++-- x86/Machregs.v | 4 ++-- 15 files changed, 53 insertions(+), 53 deletions(-) diff --git a/aarch64/Machregs.v b/aarch64/Machregs.v index b2a2308e..704c392e 100644 --- a/aarch64/Machregs.v +++ b/aarch64/Machregs.v @@ -54,9 +54,9 @@ Proof. intros. specialize (H r). InvBooleans. auto. Qed. -Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. +Global Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. -Instance Finite_mreg : Finite mreg := { +Global Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete }. diff --git a/arm/Machregs.v b/arm/Machregs.v index ae0ff6bf..dd365555 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -57,9 +57,9 @@ Proof. intros. specialize (H r). InvBooleans. auto. Qed. -Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. +Global Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. -Instance Finite_mreg : Finite mreg := { +Global Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete }. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 4755ab79..d66c7de8 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -1463,7 +1463,7 @@ End PRESERVATION. (** ** Commutation with linking *) -Instance TransfSelectionLink : TransfLink match_prog. +Global Instance TransfSelectionLink : TransfLink match_prog. Proof. red; intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2]. eapply link_match_program; eauto. diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index 3216ec50..fec3c9f8 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -1435,4 +1435,4 @@ Proof. * intros. apply PTree.elements_keys_norepet. Qed. -Instance TransfSelectionLink : TransfLink match_prog := link_match_program. +Global Instance TransfSelectionLink : TransfLink match_prog := link_match_program. diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 8e396e2a..98293888 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -1968,7 +1968,7 @@ End CORRECTNESS. (** ** Commutation with linking *) -Instance TransfCshmgenLink : TransfLink match_prog. +Global Instance TransfCshmgenLink : TransfLink match_prog. Proof. red; intros. destruct (link_linkorder _ _ _ H) as (LO1 & LO2). generalize H. diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index e3356510..504e8be1 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -1530,7 +1530,7 @@ Unset Implicit Arguments. (** ** Linking types *) -Program Instance Linker_types : Linker type := { +Global Program Instance Linker_types : Linker type := { link := fun t1 t2 => if type_eq t1 t2 then Some t1 else None; linkorder := fun t1 t2 => t1 = t2 }. @@ -1579,7 +1579,7 @@ Proof. assert (x = y) by eauto. subst y. auto. Qed. -Program Instance Linker_composite_defs : Linker (list composite_definition) := { +Global Program Instance Linker_composite_defs : Linker (list composite_definition) := { link := link_composite_defs; linkorder := @List.incl composite_definition }. @@ -1765,7 +1765,7 @@ Inductive linkorder_fundef {F: Type}: fundef F -> fundef F -> Prop := | linkorder_fundef_ext_int: forall f id sg targs tres cc, linkorder_fundef (External (EF_external id sg) targs tres cc) (Internal f). -Program Instance Linker_fundef (F: Type): Linker (fundef F) := { +Global Program Instance Linker_fundef (F: Type): Linker (fundef F) := { link := link_fundef; linkorder := linkorder_fundef }. @@ -1828,7 +1828,7 @@ Definition linkorder_program {F: Type} (p1 p2: program F) : Prop := linkorder (program_of_program p1) (program_of_program p2) /\ (forall id co, p1.(prog_comp_env)!id = Some co -> p2.(prog_comp_env)!id = Some co). -Program Instance Linker_program (F: Type): Linker (program F) := { +Global Program Instance Linker_program (F: Type): Linker (program F) := { link := link_program; linkorder := linkorder_program }. diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 67bf0e51..507e2128 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -2444,7 +2444,7 @@ End PRESERVATION. (** ** Commutation with linking *) -Instance TransfSimplExprLink : TransfLink match_prog. +Global Instance TransfSimplExprLink : TransfLink match_prog. Proof. red; intros. eapply Ctypes.link_match_program_gen; eauto. - intros. diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index e4b759c4..c133d8ea 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -2320,7 +2320,7 @@ End PRESERVATION. (** ** Commutation with linking *) -Instance TransfSimplLocalsLink : TransfLink match_prog. +Global Instance TransfSimplLocalsLink : TransfLink match_prog. Proof. red; intros. eapply Ctypes.link_match_program; eauto. - intros. diff --git a/common/Linking.v b/common/Linking.v index d23b1028..4ef83d42 100644 --- a/common/Linking.v +++ b/common/Linking.v @@ -60,7 +60,7 @@ Inductive linkorder_fundef {F: Type}: fundef F -> fundef F -> Prop := | linkorder_fundef_refl: forall fd, linkorder_fundef fd fd | linkorder_fundef_ext_int: forall f id sg, linkorder_fundef (External (EF_external id sg)) (Internal f). -Program Instance Linker_fundef (F: Type): Linker (fundef F) := { +Global Program Instance Linker_fundef (F: Type): Linker (fundef F) := { link := link_fundef; linkorder := linkorder_fundef }. @@ -114,7 +114,7 @@ Inductive linkorder_varinit: list init_data -> list init_data -> Prop := il <> nil -> init_data_list_size il = sz -> linkorder_varinit (Init_space sz :: nil) il. -Program Instance Linker_varinit : Linker (list init_data) := { +Global Program Instance Linker_varinit : Linker (list init_data) := { link := link_varinit; linkorder := linkorder_varinit }. @@ -163,7 +163,7 @@ Inductive linkorder_vardef {V: Type} {LV: Linker V}: globvar V -> globvar V -> P linkorder i1 i2 -> linkorder_vardef (mkglobvar info1 i1 ro vo) (mkglobvar info2 i2 ro vo). -Program Instance Linker_vardef (V: Type) {LV: Linker V}: Linker (globvar V) := { +Global Program Instance Linker_vardef (V: Type) {LV: Linker V}: Linker (globvar V) := { link := link_vardef; linkorder := linkorder_vardef }. @@ -189,7 +189,7 @@ Global Opaque Linker_vardef. (** A trivial linker for the trivial var info [unit]. *) -Program Instance Linker_unit: Linker unit := { +Global Program Instance Linker_unit: Linker unit := { link := fun x y => Some tt; linkorder := fun x y => True }. @@ -215,7 +215,7 @@ Inductive linkorder_def {F V: Type} {LF: Linker F} {LV: Linker V}: globdef F V - linkorder v1 v2 -> linkorder_def (Gvar v1) (Gvar v2). -Program Instance Linker_def (F V: Type) {LF: Linker F} {LV: Linker V}: Linker (globdef F V) := { +Global Program Instance Linker_def (F V: Type) {LF: Linker F} {LV: Linker V}: Linker (globdef F V) := { link := link_def; linkorder := linkorder_def }. @@ -332,7 +332,7 @@ Qed. End LINKER_PROG. -Program Instance Linker_prog (F V: Type) {LF: Linker F} {LV: Linker V} : Linker (program F V) := { +Global Program Instance Linker_prog (F V: Type) {LF: Linker F} {LV: Linker V} : Linker (program F V) := { link := link_prog; linkorder := fun p1 p2 => p1.(prog_main) = p2.(prog_main) @@ -699,7 +699,7 @@ Local Transparent Linker_fundef. - destruct (external_function_eq ef1 ef2); inv H. exists (External ef2); split; auto. simpl. rewrite dec_eq_true; auto. Qed. -Instance TransfPartialContextualLink +Global Instance TransfPartialContextualLink {A B C V: Type} {LV: Linker V} (tr_fun: C -> A -> res B) (ctx_for: program (fundef A) V -> C): @@ -714,7 +714,7 @@ Proof. - intros; subst. exists v; auto. Qed. -Instance TransfPartialLink +Global Instance TransfPartialLink {A B V: Type} {LV: Linker V} (tr_fun: A -> res B): TransfLink (fun (p1: program (fundef A) V) (p2: program (fundef B) V) => @@ -728,7 +728,7 @@ Proof. - intros; subst. exists v; auto. Qed. -Instance TransfTotallContextualLink +Global Instance TransfTotallContextualLink {A B C V: Type} {LV: Linker V} (tr_fun: C -> A -> B) (ctx_for: program (fundef A) V -> C): @@ -747,7 +747,7 @@ Proof. - intros; subst. exists v; auto. Qed. -Instance TransfTotalLink +Global Instance TransfTotalLink {A B V: Type} {LV: Linker V} (tr_fun: A -> B): TransfLink (fun (p1: program (fundef A) V) (p2: program (fundef B) V) => diff --git a/driver/Compiler.v b/driver/Compiler.v index 75247f71..b00d067e 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -209,7 +209,7 @@ Proof. intros. unfold match_if, partial_if in *. destruct (flag tt). auto. congruence. Qed. -Instance TransfIfLink {A: Type} {LA: Linker A} +Global Instance TransfIfLink {A: Type} {LA: Linker A} (flag: unit -> bool) (transf: A -> A -> Prop) (TL: TransfLink transf) : TransfLink (match_if flag transf). Proof. diff --git a/lib/Decidableplus.v b/lib/Decidableplus.v index 69ba4723..224c9640 100644 --- a/lib/Decidableplus.v +++ b/lib/Decidableplus.v @@ -27,14 +27,14 @@ Ltac decide_goal := eapply Decidable_sound; reflexivity. (** Deciding logical connectives *) -Program Instance Decidable_not (P: Prop) (dP: Decidable P) : Decidable (~ P) := { +Global Program Instance Decidable_not (P: Prop) (dP: Decidable P) : Decidable (~ P) := { Decidable_witness := negb (@Decidable_witness P dP) }. Next Obligation. rewrite negb_true_iff. split. apply Decidable_complete_alt. apply Decidable_sound_alt. Qed. -Program Instance Decidable_equiv (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P <-> Q) := { +Global Program Instance Decidable_equiv (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P <-> Q) := { Decidable_witness := Bool.eqb (@Decidable_witness P dP) (@Decidable_witness Q dQ) }. Next Obligation. @@ -46,21 +46,21 @@ Next Obligation. eapply Decidable_sound_alt; rewrite H; eapply Decidable_complete_alt; eauto. Qed. -Program Instance Decidable_and (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P /\ Q) := { +Global Program Instance Decidable_and (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P /\ Q) := { Decidable_witness := @Decidable_witness P dP && @Decidable_witness Q dQ }. Next Obligation. rewrite andb_true_iff. rewrite ! Decidable_spec. tauto. Qed. -Program Instance Decidable_or (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P \/ Q) := { +Global Program Instance Decidable_or (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P \/ Q) := { Decidable_witness := @Decidable_witness P dP || @Decidable_witness Q dQ }. Next Obligation. rewrite orb_true_iff. rewrite ! Decidable_spec. tauto. Qed. -Program Instance Decidable_implies (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P -> Q) := { +Global Program Instance Decidable_implies (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P -> Q) := { Decidable_witness := if @Decidable_witness P dP then @Decidable_witness Q dQ else true }. Next Obligation. @@ -79,28 +79,28 @@ Next Obligation. split; intros. InvBooleans. auto. subst y. apply dec_eq_true. Qed. -Program Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := { +Global Program Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := { Decidable_witness := Bool.eqb x y }. Next Obligation. apply eqb_true_iff. Qed. -Program Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := { +Global Program Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := { Decidable_witness := Nat.eqb x y }. Next Obligation. apply Nat.eqb_eq. Qed. -Program Instance Decidable_eq_positive : forall (x y : positive), Decidable (eq x y) := { +Global Program Instance Decidable_eq_positive : forall (x y : positive), Decidable (eq x y) := { Decidable_witness := Pos.eqb x y }. Next Obligation. apply Pos.eqb_eq. Qed. -Program Instance Decidable_eq_Z : forall (x y : Z), Decidable (eq x y) := { +Global Program Instance Decidable_eq_Z : forall (x y : Z), Decidable (eq x y) := { Decidable_witness := Z.eqb x y }. Next Obligation. @@ -109,35 +109,35 @@ Qed. (** Deciding order on Z *) -Program Instance Decidable_le_Z : forall (x y: Z), Decidable (x <= y) := { +Global Program Instance Decidable_le_Z : forall (x y: Z), Decidable (x <= y) := { Decidable_witness := Z.leb x y }. Next Obligation. apply Z.leb_le. Qed. -Program Instance Decidable_lt_Z : forall (x y: Z), Decidable (x < y) := { +Global Program Instance Decidable_lt_Z : forall (x y: Z), Decidable (x < y) := { Decidable_witness := Z.ltb x y }. Next Obligation. apply Z.ltb_lt. Qed. -Program Instance Decidable_ge_Z : forall (x y: Z), Decidable (x >= y) := { +Global Program Instance Decidable_ge_Z : forall (x y: Z), Decidable (x >= y) := { Decidable_witness := Z.geb x y }. Next Obligation. rewrite Z.geb_le. intuition lia. Qed. -Program Instance Decidable_gt_Z : forall (x y: Z), Decidable (x > y) := { +Global Program Instance Decidable_gt_Z : forall (x y: Z), Decidable (x > y) := { Decidable_witness := Z.gtb x y }. Next Obligation. rewrite Z.gtb_lt. intuition lia. Qed. -Program Instance Decidable_divides : forall (x y: Z), Decidable (x | y) := { +Global Program Instance Decidable_divides : forall (x y: Z), Decidable (x | y) := { Decidable_witness := Z.eqb y ((y / x) * x)%Z }. Next Obligation. @@ -153,7 +153,7 @@ Qed. (** Deciding properties over lists *) -Program Instance Decidable_forall_in_list : +Global Program Instance Decidable_forall_in_list : forall (A: Type) (l: list A) (P: A -> Prop) (dP: forall x:A, Decidable (P x)), Decidable (forall x:A, In x l -> P x) := { Decidable_witness := List.forallb (fun x => @Decidable_witness (P x) (dP x)) l @@ -164,7 +164,7 @@ Next Obligation. - eapply Decidable_complete; eauto. Qed. -Program Instance Decidable_exists_in_list : +Global Program Instance Decidable_exists_in_list : forall (A: Type) (l: list A) (P: A -> Prop) (dP: forall x:A, Decidable (P x)), Decidable (exists x:A, In x l /\ P x) := { Decidable_witness := List.existsb (fun x => @Decidable_witness (P x) (dP x)) l @@ -184,7 +184,7 @@ Class Finite (T: Type) := { (** Deciding forall and exists quantification over finite types. *) -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) := { +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) := { Decidable_witness := List.forallb (fun x => @Decidable_witness (P x) (dP x)) (@Finite_elements T fT) }. Next Obligation. @@ -193,7 +193,7 @@ Next Obligation. - eapply Decidable_complete; eauto. Qed. -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) := { +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) := { Decidable_witness := List.existsb (fun x => @Decidable_witness (P x) (dP x)) (@Finite_elements T fT) }. Next Obligation. @@ -204,21 +204,21 @@ Qed. (** Some examples of finite types. *) -Program Instance Finite_bool : Finite bool := { +Global Program Instance Finite_bool : Finite bool := { Finite_elements := false :: true :: nil }. Next Obligation. destruct x; auto. Qed. -Program Instance Finite_pair : forall (A B: Type) (fA: Finite A) (fB: Finite B), Finite (A * B) := { +Global Program Instance Finite_pair : forall (A B: Type) (fA: Finite A) (fB: Finite B), Finite (A * B) := { Finite_elements := list_prod (@Finite_elements A fA) (@Finite_elements B fB) }. Next Obligation. apply List.in_prod; eapply Finite_elements_spec. Qed. -Program Instance Finite_option : forall (A: Type) (fA: Finite A), Finite (option A) := { +Global Program Instance Finite_option : forall (A: Type) (fA: Finite A), Finite (option A) := { Finite_elements := None :: List.map (@Some A) (@Finite_elements A fA) }. Next Obligation. diff --git a/lib/Maps.v b/lib/Maps.v index 6bc6e14b..3f43d102 100644 --- a/lib/Maps.v +++ b/lib/Maps.v @@ -1604,7 +1604,7 @@ Proof. intros. transitivity a0; auto. Qed. -Instance Equal_Equivalence : Equivalence Equal := { +Global Instance Equal_Equivalence : Equivalence Equal := { Equivalence_Reflexive := Equal_refl; Equivalence_Symmetric := Equal_sym; Equivalence_Transitive := Equal_trans @@ -1633,7 +1633,7 @@ Next Obligation. unfold equiv, complement in H0. congruence. Qed. -Instance Equal_EqDec : EqDec (T.t A) Equal := Equal_dec. +Global Instance Equal_EqDec : EqDec (T.t A) Equal := Equal_dec. End EXTENSIONAL_EQUALITY. diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 9967bbae..eeca880a 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -75,9 +75,9 @@ Proof. intros. specialize (H r). InvBooleans. auto. Qed. -Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. +Global Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. -Instance Finite_mreg : Finite mreg := { +Global Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete }. diff --git a/riscV/Machregs.v b/riscV/Machregs.v index d469e594..89fa37b0 100644 --- a/riscV/Machregs.v +++ b/riscV/Machregs.v @@ -78,9 +78,9 @@ Proof. intros. specialize (H r). InvBooleans. auto. Qed. -Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. +Global Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. -Instance Finite_mreg : Finite mreg := { +Global Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete }. diff --git a/x86/Machregs.v b/x86/Machregs.v index 6f3064b8..a440bffc 100644 --- a/x86/Machregs.v +++ b/x86/Machregs.v @@ -57,9 +57,9 @@ Proof. intros. specialize (H r). InvBooleans. auto. Qed. -Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. +Global Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. -Instance Finite_mreg : Finite mreg := { +Global Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete }. -- cgit From cc3f0838d115830b2f2fba55ff8c53c212db6979 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 26 Sep 2021 17:35:58 +0200 Subject: Selectively turn some Coq 8.14 warnings off Warning "deprecated hint rewrite without locality" cannot be addressed: the suggested fix (qualify with Global or Local or [#export]) is not supported by Coq 8.11 to 8.13 ! Warning "deprecated instance without locality" is turned off for generated file cparser/Parser.v only. Menhir needs to be changed so as to generate the `Global` modifier that would silence this warning. --- Makefile | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 4a9f3772..2bc39c33 100644 --- a/Makefile +++ b/Makefile @@ -53,11 +53,21 @@ endif # deprecated-ident-entry: # warning introduced in 8.13 # suggested change (use `name` instead of `ident`) supported since 8.13 +# deprecated-hint-rewrite-without-locality: +# warning introduced in 8.14 +# suggested change (add Global or Local or [#export] modifier) +# is not supported in 8.13 nor in 8.11, but was supported in 8.9 (go figure) +# deprecated-instance-without-locality: +# warning introduced in 8.14 +# triggered by Menhir-generated files, to be solved upstream in Menhir COQCOPTS ?= \ -w -undeclared-scope \ -w -unused-pattern-matching-variable \ - -w -deprecated-ident-entry + -w -deprecated-ident-entry \ + -w -deprecated-hint-rewrite-without-locality + +cparser/Parser.vo: COQCOPTS += -w -deprecated-instance-without-locality COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS) COQDEP="$(COQBIN)coqdep" $(COQINCLUDES) -- cgit From af2b004f567e5437904ffa168cf1d79d7b176a00 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 1 Oct 2021 11:12:14 +0200 Subject: Add Coq 8.14.0 to the supported versions of Coq --- configure | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/configure b/configure index 10f60262..1b224319 100755 --- a/configure +++ b/configure @@ -504,19 +504,19 @@ missingtools=false echo "Testing Coq... " | tr -d '\n' coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p') case "$coq_ver" in - 8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0|8.12.1|8.12.2|8.13.0|8.13.1|8.13.2) + 8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0|8.12.1|8.12.2|8.13.0|8.13.1|8.13.2|8.14.0) echo "version $coq_ver -- good!";; ?*) echo "version $coq_ver -- UNSUPPORTED" if $ignore_coq_version; then echo "Warning: this version of Coq is unsupported, proceed at your own risks." else - echo "Error: CompCert requires a version of Coq between 8.9.0 and 8.13.2" + echo "Error: CompCert requires a version of Coq between 8.9.0 and 8.14.0" missingtools=true fi;; "") echo "NOT FOUND" - echo "Error: make sure Coq version 8.12.2 is installed." + echo "Error: make sure Coq version 8.13.2 is installed." missingtools=true;; esac -- cgit