diff options
Diffstat (limited to 'src/hls/Pipeline.v')
| -rw-r--r-- | src/hls/Pipeline.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/hls/Pipeline.v b/src/hls/Pipeline.v index 7f1485a..67ab1f5 100644 --- a/src/hls/Pipeline.v +++ b/src/hls/Pipeline.v @@ -16,7 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -Require Import compcert.lib.Maps. +(*Require Import compcert.lib.Maps. Require Import compcert.common.AST. Require Import compcert.backend.RTL. @@ -26,3 +26,4 @@ Definition transf_fundef := transf_fundef pipeline. Definition transf_program : program -> program := transform_program transf_fundef. +*) |