aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/PipelineOp.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/hls/PipelineOp.v')
-rw-r--r--src/hls/PipelineOp.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/PipelineOp.v b/src/hls/PipelineOp.v
index 90ccea0..76634a6 100644
--- a/src/hls/PipelineOp.v
+++ b/src/hls/PipelineOp.v
@@ -34,7 +34,7 @@ Require Import vericert.hls.FunctionalUnits.
Require Import vericert.common.Monad.
Module OptionExtra := MonadExtra(Option).
-Import OptionExtra.MonadNotation.
+(*Import OptionExtra.MonadNotation.*)
Local Open Scope positive.