diff options
Diffstat (limited to 'src/translation/HTLgenproof.v')
| -rw-r--r-- | src/translation/HTLgenproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 2f296f2..6dd0688 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -18,7 +18,7 @@ From compcert Require RTL Registers AST Integers. From compcert Require Import Globalenvs Memory. -From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra. +From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra ZExtra. From coqup Require HTL Verilog. Require Import Lia. |