diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-01-21 22:18:50 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-21 22:18:50 +0000 |
| commit | 3addff470c8faeb6876c63575184caa0aa829e28 (patch) | |
| tree | 84684245fd8e57b96b28ed4f486242c5bc3e0732 /src/hls/HTLPargen.v | |
| parent | ff4257c78aeefee69f3b17702153296c8c639348 (diff) | |
| download | vericert-3addff470c8faeb6876c63575184caa0aa829e28.tar.gz vericert-3addff470c8faeb6876c63575184caa0aa829e28.zip | |
Fix imports in Coq modules
Diffstat (limited to 'src/hls/HTLPargen.v')
| -rw-r--r-- | src/hls/HTLPargen.v | 20 |
1 files changed, 15 insertions, 5 deletions
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 474dfef..70c0454 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -16,11 +16,21 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From compcert Require Errors Globalenvs Integers. -From compcert Require Import Maps AST. -From vericert Require Import Verilog RTLPar HTL Vericertlib AssocMap ValueInt Statemonad. - -Import Lia. +Require Import Coq.micromega.Lia. + +Require Import compcert.common.AST. +Require compcert.common.Errors. +Require compcert.common.Globalenvs. +Require compcert.lib.Integers. +Require Import compcert.lib.Maps. + +Require Import vericert.common.Statemonad. +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.Verilog. +Require Import vericert.hls.RTLPar. +Require Import vericert.hls.HTL. +Require Import vericert.hls.AssocMap. +Require Import vericert.hls.ValueInt. Hint Resolve AssocMap.gempty : htlh. Hint Resolve AssocMap.gso : htlh. |