diff options
Diffstat (limited to 'src/hls/HTLgen.v')
| -rw-r--r-- | src/hls/HTLgen.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 79fcc53..04595af 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -35,11 +35,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; @@ -86,10 +86,10 @@ Module HTLState <: State. (exists x, (st_externctrl s2) ! n = Some x) -> (n >= st_freshreg s1)%positive) -> 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. split; try solve [ auto with htlh; crush ]. Qed. |