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/Compiler.v | |
| parent | ff4257c78aeefee69f3b17702153296c8c639348 (diff) | |
| download | vericert-3addff470c8faeb6876c63575184caa0aa829e28.tar.gz vericert-3addff470c8faeb6876c63575184caa0aa829e28.zip | |
Fix imports in Coq modules
Diffstat (limited to 'src/Compiler.v')
| -rw-r--r-- | src/Compiler.v | 76 |
1 files changed, 33 insertions, 43 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index ce36d5b..0578f57 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -36,49 +36,39 @@ Imports We first need to import all of the modules that are used in the correctness proof, which includes all of the passes that are performed in Vericert and the CompCert front end. |*) -From vericert Require Import HTLgenproof. - -From compcert.common Require Import - Errors - Linking. - -From compcert.lib Require Import - Coqlib. - -From compcert.backend Require - Selection - RTL - RTLgen - Tailcall - Inlining - Renumber - Constprop - CSE - Deadcode - Unusedglob. - -From compcert.cfrontend Require - Csyntax - SimplExpr - SimplLocals - Cshmgen - Cminorgen. - -From compcert.driver Require - Compiler. - -From vericert Require - Verilog - Veriloggen - Veriloggenproof - HTLgen - RTLBlock - RTLBlockgen - RTLPargen - HTLPargen - Pipeline. - -From compcert Require Import Smallstep. +Require compcert.backend.Selection. +Require compcert.backend.RTL. +Require compcert.backend.RTLgen. +Require compcert.backend.Tailcall. +Require compcert.backend.Inlining. +Require compcert.backend.Renumber. +Require compcert.backend.Constprop. +Require compcert.backend.CSE. +Require compcert.backend.Deadcode. +Require compcert.backend.Unusedglob. +Require compcert.cfrontend.Csyntax. +Require compcert.cfrontend.SimplExpr. +Require compcert.cfrontend.SimplLocals. +Require compcert.cfrontend.Cshmgen. +Require compcert.cfrontend.Cminorgen. +Require compcert.driver.Compiler. + +Require Import compcert.common.Errors. +Require Import compcert.common.Linking. +Require Import compcert.common.Smallstep. +Require Import compcert.lib.Coqlib. + +Require vericert.hls.Verilog. +Require vericert.hls.Veriloggen. +Require vericert.hls.Veriloggenproof. +Require vericert.hls.HTLgen. +Require vericert.hls.RTLBlock. +Require vericert.hls.RTLBlockgen. +Require vericert.hls.RTLPargen. +Require vericert.hls.HTLPargen. +Require vericert.hls.Pipeline. + +Require Import vericert.hls.HTLgenproof. (*| Declarations |