diff options
Diffstat (limited to 'src/hls')
| -rw-r--r-- | src/hls/HashTree.v | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/src/hls/HashTree.v b/src/hls/HashTree.v index 0aa0dd9..f3c57a8 100644 --- a/src/hls/HashTree.v +++ b/src/hls/HashTree.v @@ -16,20 +16,9 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -Require Import compcert.backend.Registers. -Require Import compcert.common.AST. -Require Import compcert.common.Globalenvs. -Require Import compcert.common.Memory. -Require Import compcert.common.Values. -Require Import compcert.lib.Floats. -Require Import compcert.lib.Integers. Require Import compcert.lib.Maps. -Require compcert.verilog.Op. Require Import vericert.common.Vericertlib. -Require Import vericert.hls.RTLBlock. -Require Import vericert.hls.RTLPar. -Require Import vericert.hls.RTLBlockInstr. #[local] Open Scope positive. |