diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-10-18 17:05:46 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-10-18 17:05:46 +0100 |
| commit | fbfa988072ce2eba808b9a6631af5f8e86cd9df0 (patch) | |
| tree | 5146e558d5c9c6e9a399225eed0784b8dc12558f /src/hls/HTLgenspec.v | |
| parent | 603768a49eac2005729dd03e723ff6c5a6b292f7 (diff) | |
| parent | fe06668f0de56635efe55310d7a64289a37c1d90 (diff) | |
| download | vericert-fbfa988072ce2eba808b9a6631af5f8e86cd9df0.tar.gz vericert-fbfa988072ce2eba808b9a6631af5f8e86cd9df0.zip | |
Merge branch 'master' into dev/michalisdev/michalis
Diffstat (limited to 'src/hls/HTLgenspec.v')
| -rw-r--r-- | src/hls/HTLgenspec.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 3c52657..c38b4e6 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -149,16 +149,16 @@ Inductive tr_module (ge : RTL.genv) (f : RTL.function) : module -> Prop := (clk > rst)%positive -> externctrl_ordering externctrl clk -> tr_module ge f m. -Hint Constructors tr_module : htlspec. +#[local] Hint Constructors tr_module : htlspec. -Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. -Hint Resolve Maps.PTree.elements_correct : htlspec. -Hint Resolve Maps.PTree.gss : htlspec. -Hint Resolve PTree.elements_complete : htlspec. -Hint Resolve -> Z.leb_le : htlspec. +#[local] Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. +#[local] Hint Resolve Maps.PTree.elements_correct : htlspec. +#[local] Hint Resolve Maps.PTree.gss : htlspec. +#[local] Hint Resolve PTree.elements_complete : htlspec. +#[local] Hint Resolve -> Z.leb_le : htlspec. -Hint Unfold block : htlspec. -Hint Unfold nonblock : htlspec. +#[local] Hint Unfold block : htlspec. +#[local] Hint Unfold nonblock : htlspec. Remark bind_inversion: forall (A B: Type) (f: mon A) (g: A -> mon B) @@ -395,7 +395,7 @@ Proof. assert (n < Datatypes.length args)%nat by eauto using nth_error_length. eauto. Qed. -Hint Resolve map_externctrl_params_spec : htlspec. +#[local] Hint Resolve map_externctrl_params_spec : htlspec. Lemma externctrl_params_mapped_trans : forall s s' args params fn, externctrl_params_mapped args params (st_externctrl s) fn -> @@ -493,7 +493,7 @@ Proof. - eapply IHl; eauto. intuition crush. Qed. -Hint Resolve iter_expand_instr_spec : htlspec. +#[local] Hint Resolve iter_expand_instr_spec : htlspec. Lemma map_incr_some : forall {A} map (s s' : st) idx (x : A), (map s) ! idx = Some x -> |