diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-02 11:12:45 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-02 11:12:45 +0100 |
| commit | 564fb33a504d7611d73bbe5e20b23453e141ed3d (patch) | |
| tree | 441cd64ddf97c3288693a1041904a8a502715754 /src/hls/HTLgenspec.v | |
| parent | b8107dbffc3c9a27b7beb4014883a55102389a29 (diff) | |
| download | vericert-564fb33a504d7611d73bbe5e20b23453e141ed3d.tar.gz vericert-564fb33a504d7611d73bbe5e20b23453e141ed3d.zip | |
Simplify some HTLgenspec proofs
Diffstat (limited to 'src/hls/HTLgenspec.v')
| -rw-r--r-- | src/hls/HTLgenspec.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 77e8c3d..f3c375c 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -222,7 +222,7 @@ Lemma map_externctrl_datapath_trans : map_externctrl om sig s = OK x s' i -> s.(st_datapath) = s'.(st_datapath). Proof. - intros. monadInv H. apply create_reg_datapath_trans in EQ. auto. + intros. monadInv H. auto_hyp create_reg_datapath_trans. Qed. Hint Resolve map_externctrl_datapath_trans : htlspec. @@ -231,7 +231,7 @@ Lemma map_externctrl_controllogic_trans : map_externctrl om sig s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic). Proof. - intros. monadInv H. apply create_reg_controllogic_trans in EQ. auto. + intros. monadInv H. auto_hyp create_reg_controllogic_trans. Qed. Hint Resolve map_externctrl_datapath_trans : htlspec. |