From f06e5fc0ee651c3ffe357c3c3302ca1517381b4c Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 9 Oct 2021 14:30:03 +0100 Subject: Fix warnings for Coq 8.13.2 --- docs | 2 +- src/common/Monad.v | 4 ++-- src/common/Vericertlib.v | 8 ++++---- src/hls/Array.v | 10 ++++----- src/hls/AssocMap.v | 52 ++++++++++++++++++++++++++++++----------------- src/hls/HTL.v | 2 +- src/hls/HTLgen.v | 14 ++++++------- src/hls/Sat.v | 24 +++++++++++----------- src/hls/Verilog.v | 18 ++++++++-------- src/hls/Veriloggenproof.v | 22 ++++++++++---------- 10 files changed, 85 insertions(+), 71 deletions(-) diff --git a/docs b/docs index 42e19f2..f852380 160000 --- a/docs +++ b/docs @@ -1 +1 @@ -Subproject commit 42e19f2b20c907505a28486a8071147ed6c610fb +Subproject commit f85238030a96a082f19446a7998da97123ce7026 diff --git a/src/common/Monad.v b/src/common/Monad.v index 5e8385e..fcbe527 100644 --- a/src/common/Monad.v +++ b/src/common/Monad.v @@ -40,10 +40,10 @@ Module MonadExtra(M : Monad). Notation "'do' X <- A ; B" := (bind A (fun X => B)) - (at level 200, X ident, A at level 100, B at level 200). + (at level 200, X name, A at level 100, B at level 200). Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B)) - (at level 200, X ident, Y ident, A at level 100, B at level 200). + (at level 200, X name, Y name, A at level 100, B at level 200). End MonadNotation. Import MonadNotation. diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index b58ebd4..389a74f 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -34,7 +34,7 @@ Require Import vericert.common.Show. (* Depend on CompCert for the basic library, as they declare and prove some useful theorems. *) -Local Open Scope Z_scope. +#[local] Open Scope Z_scope. (* This tactic due to Clement Pit-Claudel with some minor additions by JDP to allow the result to be named: https://pit-claudel.fr/clement/MSc/#org96a1b5f *) @@ -190,8 +190,8 @@ Ltac liapp := Ltac crush := simplify; try discriminate; try congruence; try lia; liapp; try assumption; try (solve [auto]). -Global Opaque Nat.div. -Global Opaque Z.mul. +#[global] Opaque Nat.div. +#[global] Opaque Z.mul. (* Definition const (A B : Type) (a : A) (b : B) : A := a. @@ -231,7 +231,7 @@ Definition join {A : Type} (a : option (option A)) : option A := Module Notation. Notation "'do' X <- A ; B" := (bind A (fun X => B)) - (at level 200, X ident, A at level 100, B at level 200). + (at level 200, X name, A at level 100, B at level 200). End Notation. End Option. diff --git a/src/hls/Array.v b/src/hls/Array.v index dec1335..0f5ae02 100644 --- a/src/hls/Array.v +++ b/src/hls/Array.v @@ -51,7 +51,7 @@ Lemma list_set_spec1 {A : Type} : Proof. induction l; intros; destruct i; crush; firstorder. intuition. Qed. -Hint Resolve list_set_spec1 : array. +#[export] Hint Resolve list_set_spec1 : array. Lemma list_set_spec2 {A : Type} : forall l i (x : A) d, @@ -59,7 +59,7 @@ Lemma list_set_spec2 {A : Type} : Proof. induction l; intros; destruct i; crush; firstorder. intuition. Qed. -Hint Resolve list_set_spec2 : array. +#[export] Hint Resolve list_set_spec2 : array. Lemma list_set_spec3 {A : Type} : forall l i1 i2 (x : A), @@ -68,7 +68,7 @@ Lemma list_set_spec3 {A : Type} : Proof. induction l; intros; destruct i1; destruct i2; crush; firstorder. Qed. -Hint Resolve list_set_spec3 : array. +#[export] Hint Resolve list_set_spec3 : array. Lemma array_set_wf {A : Type} : forall l ln i (x : A), @@ -95,7 +95,7 @@ Proof. unfold array_set. crush. eauto with array. Qed. -Hint Resolve array_set_spec1 : array. +#[export] Hint Resolve array_set_spec1 : array. Lemma array_set_spec2 {A : Type} : forall a i (x : A) d, @@ -107,7 +107,7 @@ Proof. unfold array_set. crush. eauto with array. Qed. -Hint Resolve array_set_spec2 : array. +#[export] Hint Resolve array_set_spec2 : array. Lemma array_set_len {A : Type} : forall a i (x : A), diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v index 98eda9c..8dbc6b2 100644 --- a/src/hls/AssocMap.v +++ b/src/hls/AssocMap.v @@ -29,9 +29,8 @@ Module AssocMap := Maps.PTree. Module AssocMapExt. Import AssocMap. - Hint Resolve elements_correct elements_complete - elements_keys_norepet : assocmap. - Hint Resolve gso gss : assocmap. + #[export] Hint Resolve elements_correct elements_complete elements_keys_norepet : assocmap. + #[export] Hint Resolve gso gss : assocmap. Section Operations. @@ -55,7 +54,6 @@ Module AssocMapExt. forall am, merge (empty A) am = am. Proof. auto. Qed. - Hint Resolve merge_base_1 : assocmap. Lemma merge_base_2 : forall am, @@ -65,7 +63,6 @@ Module AssocMapExt. destruct am; trivial. destruct o; trivial. Qed. - Hint Resolve merge_base_2 : assocmap. Lemma merge_add_assoc : forall r am am' v, @@ -74,7 +71,6 @@ Module AssocMapExt. induction r; intros; destruct am; destruct am'; try (destruct o); simpl; try rewrite IHr; try reflexivity. Qed. - Hint Resolve merge_add_assoc : assocmap. Lemma merge_correct_1 : forall am bm k v, @@ -84,7 +80,6 @@ Module AssocMapExt. induction am; intros; destruct k; destruct bm; try (destruct o); simpl; try rewrite gempty in H; try discriminate; try assumption; auto. Qed. - Hint Resolve merge_correct_1 : assocmap. Lemma merge_correct_2 : forall am bm k v, @@ -95,7 +90,6 @@ Module AssocMapExt. induction am; intros; destruct k; destruct bm; try (destruct o); simpl; try rewrite gempty in H; try discriminate; try assumption; auto. Qed. - Hint Resolve merge_correct_2 : assocmap. Lemma merge_correct_3 : forall am bm k, @@ -106,7 +100,6 @@ Module AssocMapExt. induction am; intros; destruct k; destruct bm; try (destruct o); simpl; try rewrite gempty in H; try discriminate; try assumption; auto. Qed. - Hint Resolve merge_correct_3 : assocmap. Definition merge_fold (am bm : t A) : t A := fold_right (fun p a => set (fst p) (snd p) a) bm (elements am). @@ -130,7 +123,6 @@ Module AssocMapExt. apply IHl. contradiction. contradiction. simpl. rewrite gso; try assumption. apply IHl. assumption. inversion H0. subst. assumption. Qed. - Hint Resolve add_assoc : assocmap. Lemma not_in_assoc : forall k v l bm, @@ -145,7 +137,6 @@ Module AssocMapExt. simpl in *; apply Decidable.not_or in H; destruct H. contradiction. rewrite AssocMap.gso; auto. Qed. - Hint Resolve not_in_assoc : assocmap. Lemma elements_iff : forall am k, @@ -158,14 +149,22 @@ Module AssocMapExt. exists (snd x). apply elements_complete. assert (x = (fst x, snd x)) by apply surjective_pairing. rewrite H in H0; assumption. Qed. - Hint Resolve elements_iff : assocmap. + + #[local] Hint Resolve merge_base_1 : core. + #[local] Hint Resolve merge_base_2 : core. + #[local] Hint Resolve merge_add_assoc : core. + #[local] Hint Resolve merge_correct_1 : core. + #[local] Hint Resolve merge_correct_2 : core. + #[local] Hint Resolve merge_correct_3 : core. + #[local] Hint Resolve add_assoc : core. + #[local] Hint Resolve not_in_assoc : core. + #[local] Hint Resolve elements_iff : core. Lemma elements_correct' : forall am k, ~ (exists v, get k am = Some v) <-> ~ List.In k (List.map (@fst _ A) (elements am)). - Proof. auto using not_iff_compat with assocmap. Qed. - Hint Resolve elements_correct' : assocmap. + Proof. auto using not_iff_compat. Qed. Lemma elements_correct_none : forall am k, @@ -175,31 +174,46 @@ Module AssocMapExt. intros. apply elements_correct'. unfold not. intros. destruct H0. rewrite H in H0. discriminate. Qed. - Hint Resolve elements_correct_none : assocmap. Lemma merge_fold_add : forall k v am bm, am ! k = Some v -> (merge_fold am bm) ! k = Some v. Proof. unfold merge_fold; auto with assocmap. Qed. - Hint Resolve merge_fold_add : assocmap. + + #[local] Hint Resolve elements_correct' : core. + #[local] Hint Resolve elements_correct_none : core. + #[local] Hint Resolve merge_fold_add : core. Lemma merge_fold_not_in : forall k v am bm, get k am = None -> get k bm = Some v -> get k (merge_fold am bm) = Some v. - Proof. intros. apply not_in_assoc; auto with assocmap. Qed. - Hint Resolve merge_fold_not_in : assocmap. + Proof. intros. apply not_in_assoc; auto. Qed. Lemma merge_fold_base : forall am, merge_fold (empty A) am = am. Proof. auto. Qed. - Hint Resolve merge_fold_base : assocmap. End Operations. + #[export] Hint Resolve merge_base_1 : assocmap. + #[export] Hint Resolve merge_base_2 : assocmap. + #[export] Hint Resolve merge_add_assoc : assocmap. + #[export] Hint Resolve merge_correct_1 : assocmap. + #[export] Hint Resolve merge_correct_2 : assocmap. + #[export] Hint Resolve merge_correct_3 : assocmap. + #[export] Hint Resolve add_assoc : assocmap. + #[export] Hint Resolve not_in_assoc : assocmap. + #[export] Hint Resolve elements_iff : assocmap. + #[export] Hint Resolve elements_correct' : assocmap. + #[export] Hint Resolve merge_fold_not_in : assocmap. + #[export] Hint Resolve merge_fold_base : assocmap. + #[export] Hint Resolve elements_correct_none : assocmap. + #[export] Hint Resolve merge_fold_add : assocmap. + End AssocMapExt. Import AssocMapExt. diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 61ea541..8cebbfd 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -227,7 +227,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := mst = mod_st m -> step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa). -Hint Constructors step : htl. +#[export] Hint Constructors step : htl. Inductive initial_state (p: program): state -> Prop := | initial_state_intro: forall b m0 m, diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 4d60a24..3f4e513 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -33,11 +33,11 @@ Require Import vericert.hls.HTL. Require Import vericert.hls.ValueInt. Require Import vericert.hls.Verilog. -Hint Resolve AssocMap.gempty : htlh. -Hint Resolve AssocMap.gso : htlh. -Hint Resolve AssocMap.gss : htlh. -Hint Resolve Ple_refl : htlh. -Hint Resolve Ple_succ : htlh. +#[local] Hint Resolve AssocMap.gempty : htlh. +#[local] Hint Resolve AssocMap.gso : htlh. +#[local] Hint Resolve AssocMap.gss : htlh. +#[local] Hint Resolve Ple_refl : htlh. +#[local] Hint Resolve Ple_succ : htlh. Record state: Type := mkstate { st_st : reg; @@ -74,10 +74,10 @@ Module HTLState <: State. s1.(st_controllogic)!n = None \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) -> st_incr s1 s2. - Hint Constructors st_incr : htlh. + #[export] Hint Constructors st_incr : htlh. Definition st_prop := st_incr. - Hint Unfold st_prop : htlh. + #[export] Hint Unfold st_prop : htlh. Lemma st_refl : forall s, st_prop s s. Proof. auto with htlh. Qed. diff --git a/src/hls/Sat.v b/src/hls/Sat.v index 679f5ec..098eef1 100644 --- a/src/hls/Sat.v +++ b/src/hls/Sat.v @@ -146,7 +146,7 @@ Lemma contradictory_assignment : forall s l cl a, tauto. Qed. -Local Hint Resolve contradictory_assignment : core. +#[local] Hint Resolve contradictory_assignment : core. (** Augment an assignment with a new mapping. *) Definition upd (a : asgn) (l : lit) : asgn := @@ -163,7 +163,7 @@ Lemma satLit_upd_eq : forall l a, destruct (eq_nat_dec (snd l) (snd l)); tauto. Qed. -Local Hint Resolve satLit_upd_eq : core. +#[local] Hint Resolve satLit_upd_eq : core. Lemma satLit_upd_neq : forall v l s a, v <> snd l @@ -173,7 +173,7 @@ Lemma satLit_upd_neq : forall v l s a, destruct (eq_nat_dec v (snd l)); tauto. Qed. -Local Hint Resolve satLit_upd_neq : core. +#[local] Hint Resolve satLit_upd_neq : core. Lemma satLit_upd_neq2 : forall v l s a, v <> snd l @@ -183,7 +183,7 @@ Lemma satLit_upd_neq2 : forall v l s a, destruct (eq_nat_dec v (snd l)); tauto. Qed. -Local Hint Resolve satLit_upd_neq2 : core. +#[local] Hint Resolve satLit_upd_neq2 : core. Lemma satLit_contra : forall s l a cl, s <> fst l @@ -194,7 +194,7 @@ Lemma satLit_contra : forall s l a cl, assert False; intuition. Qed. -Local Hint Resolve satLit_contra : core. +#[local] Hint Resolve satLit_contra : core. (** Here's the tactic that I used to discharge ##all## proof obligations in my implementations of the four functions you will define. @@ -288,7 +288,7 @@ Lemma satLit_idem_lit : forall l a l', destruct (eq_nat_dec (snd l') (snd l)); congruence. Qed. -Local Hint Resolve satLit_idem_lit : core. +#[local] Hint Resolve satLit_idem_lit : core. Lemma satLit_idem_clause : forall l a cl, satLit l a @@ -297,7 +297,7 @@ Lemma satLit_idem_clause : forall l a cl, induction cl; simpl; intuition. Qed. -Local Hint Resolve satLit_idem_clause : core. +#[local] Hint Resolve satLit_idem_clause : core. Lemma satLit_idem_formula : forall l a fm, satLit l a @@ -306,7 +306,7 @@ Lemma satLit_idem_formula : forall l a fm, induction fm; simpl; intuition. Qed. -Local Hint Resolve satLit_idem_formula : core. +#[local] Hint Resolve satLit_idem_formula : core. (** Challenge 2: Write this function that updates an entire formula to reflect setting a literal to true. @@ -349,7 +349,7 @@ Eval compute in setFormulaSimple (((false, 1) :: nil) :: nil) (true, 0). Eval compute in setFormulaSimple (((false, 1) :: (true, 0) :: nil) :: nil) (true, 0). Eval compute in setFormulaSimple (((false, 1) :: (false, 0) :: nil) :: nil) (true, 0).*) -Local Hint Extern 1 False => discriminate : core. +#[local] Hint Extern 1 False => discriminate : core. Local Hint Extern 1 False => match goal with @@ -366,7 +366,7 @@ Definition findUnitClause : forall (fm: formula), match fm with | nil => inright _ | (l :: nil) :: fm' => inleft (exist _ l _) - | cl :: fm' => + | _ :: fm' => match findUnitClause fm' with | inleft (exist _ l _) => inleft (exist _ l _) | inright H => inright _ @@ -387,7 +387,7 @@ Lemma unitClauseTrue : forall l a fm, inversion H; subst; simpl in H0; intuition. Qed. -Local Hint Resolve unitClauseTrue : core. +#[local] Hint Resolve unitClauseTrue : core. (** Final challenge: Implement unit propagation. The return type of [unitPropagate] signifies that three results are possible: @@ -447,7 +447,7 @@ Definition chooseSplit (fm : formula) := Definition negate (l : lit) := (negb (fst l), snd l). -Local Hint Unfold satFormula : core. +#[local] Hint Unfold satFormula : core. Lemma satLit_dec : forall l a, {satLit l a} + {satLit (negate l) a}. diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index 1dc7e99..cee1d60 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -414,7 +414,7 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop expr_runp fext reg stack fs vf -> valueToBool vc = false -> expr_runp fext reg stack (Vternary c ts fs) vf. -Hint Constructors expr_runp : verilog. +#[export] Hint Constructors expr_runp : verilog. Definition handle_opt {A : Type} (err : errmsg) (val : option A) : res A := @@ -512,7 +512,7 @@ Inductive stmnt_runp: fext -> reg_associations -> arr_associations -> stmnt_runp f asr asa (Vnonblock lhs rhs) asr (nonblock_arr r i asa rhsval). -Hint Constructors stmnt_runp : verilog. +#[export] Hint Constructors stmnt_runp : verilog. Inductive mi_stepp : fext -> reg_associations -> arr_associations -> module_item -> reg_associations -> arr_associations -> Prop := @@ -526,7 +526,7 @@ Inductive mi_stepp : fext -> reg_associations -> arr_associations -> | mi_stepp_Vdecl : forall f sr0 sa0 d, mi_stepp f sr0 sa0 (Vdeclaration d) sr0 sa0. -Hint Constructors mi_stepp : verilog. +#[export] Hint Constructors mi_stepp : verilog. Inductive mi_stepp_negedge : fext -> reg_associations -> arr_associations -> module_item -> reg_associations -> arr_associations -> Prop := @@ -540,7 +540,7 @@ Inductive mi_stepp_negedge : fext -> reg_associations -> arr_associations -> | mi_stepp_negedge_Vdecl : forall f sr0 sa0 d, mi_stepp_negedge f sr0 sa0 (Vdeclaration d) sr0 sa0. -Hint Constructors mi_stepp : verilog. +#[export] Hint Constructors mi_stepp : verilog. Inductive mis_stepp : fext -> reg_associations -> arr_associations -> list module_item -> reg_associations -> arr_associations -> Prop := @@ -552,7 +552,7 @@ Inductive mis_stepp : fext -> reg_associations -> arr_associations -> | mis_stepp_Nil : forall f sr sa, mis_stepp f sr sa nil sr sa. -Hint Constructors mis_stepp : verilog. +#[export] Hint Constructors mis_stepp : verilog. Inductive mis_stepp_negedge : fext -> reg_associations -> arr_associations -> list module_item -> reg_associations -> arr_associations -> Prop := @@ -564,7 +564,7 @@ Inductive mis_stepp_negedge : fext -> reg_associations -> arr_associations -> | mis_stepp_negedge_Nil : forall f sr sa, mis_stepp_negedge f sr sa nil sr sa. -Hint Constructors mis_stepp : verilog. +#[export] Hint Constructors mis_stepp : verilog. Local Close Scope error_monad_scope. @@ -620,7 +620,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := mst = mod_st m -> step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa). -Hint Constructors step : verilog. +#[export] Hint Constructors step : verilog. Inductive initial_state (p: program): state -> Prop := | initial_state_intro: forall b m0 m, @@ -678,7 +678,7 @@ Proof. learn (H1 _ H2) end; crush). Qed. -Hint Resolve expr_runp_determinate : verilog. +#[export] Hint Resolve expr_runp_determinate : verilog. Lemma location_is_determinate : forall f asr asa e l, @@ -727,7 +727,7 @@ Lemma stmnt_runp_determinate : learn (H1 _ _ H2) end; crush). Qed. -Hint Resolve stmnt_runp_determinate : verilog. +#[export] Hint Resolve stmnt_runp_determinate : verilog. Lemma mi_stepp_determinate : forall f asr0 asa0 m asr1 asa1, diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v index b621632..d1494ec 100644 --- a/src/hls/Veriloggenproof.v +++ b/src/hls/Veriloggenproof.v @@ -115,7 +115,7 @@ Lemma Zle_relax : p < q <= r -> p <= q <= r. Proof. lia. Qed. -Hint Resolve Zle_relax : verilogproof. +#[local] Hint Resolve Zle_relax : verilogproof. Lemma transl_in : forall l p, @@ -202,7 +202,7 @@ Proof. eapply IHl. auto. inv NOREP. auto. eassumption. inv IN. inv H. contradiction. apply H. trivial. assumption. Qed. -Hint Resolve transl_list_correct : verilogproof. +#[local] Hint Resolve transl_list_correct : verilogproof. Lemma pc_wf : forall A m p v, @@ -223,7 +223,7 @@ Proof. - intros. constructor. - intros. simplify. econstructor. constructor. auto. Qed. -Hint Resolve mis_stepp_decl : verilogproof. +#[local] Hint Resolve mis_stepp_decl : verilogproof. Lemma mis_stepp_negedge_decl : forall l asr asa f, @@ -233,7 +233,7 @@ Proof. - intros. constructor. - intros. simplify. econstructor. constructor. auto. Qed. -Hint Resolve mis_stepp_negedge_decl : verilogproof. +#[local] Hint Resolve mis_stepp_negedge_decl : verilogproof. Lemma mod_entrypoint_equiv m : mod_entrypoint (transl_module m) = HTL.mod_entrypoint m. Proof. unfold transl_module; intros; destruct (HTL.mod_ram m) eqn:?; crush. Qed. @@ -348,7 +348,7 @@ Section CORRECTNESS. Lemma symbols_preserved: forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof. intros. eapply (Genv.find_symbol_match TRANSL). Qed. - Hint Resolve symbols_preserved : verilogproof. + #[local] Hint Resolve symbols_preserved : verilogproof. Lemma function_ptr_translated: forall (b: Values.block) (f: HTL.fundef), @@ -359,7 +359,7 @@ Section CORRECTNESS. intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto. intros (cu & tf & P & Q & R); exists tf; auto. Qed. - Hint Resolve function_ptr_translated : verilogproof. + #[local] Hint Resolve function_ptr_translated : verilogproof. Lemma functions_translated: forall (v: Values.val) (f: HTL.fundef), @@ -370,14 +370,14 @@ Section CORRECTNESS. intros. exploit (Genv.find_funct_match TRANSL); eauto. intros (cu & tf & P & Q & R); exists tf; auto. Qed. - Hint Resolve functions_translated : verilogproof. + #[local] Hint Resolve functions_translated : verilogproof. Lemma senv_preserved: Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). Proof. intros. eapply (Genv.senv_match TRANSL). Qed. - Hint Resolve senv_preserved : verilogproof. + #[local] Hint Resolve senv_preserved : verilogproof. Ltac unfold_replace := match goal with @@ -502,7 +502,7 @@ Section CORRECTNESS. - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. repeat rewrite_eq. apply match_state. assumption. Qed. - Hint Resolve transl_step_correct : verilogproof. + #[local] Hint Resolve transl_step_correct : verilogproof. Lemma transl_initial_states : forall s1 : Smallstep.state (HTL.semantics prog), @@ -520,7 +520,7 @@ Section CORRECTNESS. inv B. eauto. constructor. Qed. - Hint Resolve transl_initial_states : verilogproof. + #[local] Hint Resolve transl_initial_states : verilogproof. Lemma transl_final_states : forall (s1 : Smallstep.state (HTL.semantics prog)) @@ -532,7 +532,7 @@ Section CORRECTNESS. Proof. intros. inv H0. inv H. inv H3. constructor. reflexivity. Qed. - Hint Resolve transl_final_states : verilogproof. + #[local] Hint Resolve transl_final_states : verilogproof. Theorem transf_program_correct: forward_simulation (HTL.semantics prog) (Verilog.semantics tprog). -- cgit