diff options
Diffstat (limited to 'src/hls/Memorygen.v')
| -rw-r--r-- | src/hls/Memorygen.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v index 4ff4a19..e28bbc7 100644 --- a/src/hls/Memorygen.v +++ b/src/hls/Memorygen.v @@ -44,7 +44,7 @@ Local Open Scope assocmap. #[local] Hint Resolve max_reg_stmnt_lt_stmnt_tree : mgen. #[local] Hint Resolve max_stmnt_lt_module : mgen. -Lemma int_eq_not_false : forall x, Int.eq x (Int.not x) = false. +(*Lemma int_eq_not_false : forall x, Int.eq x (Int.not x) = false. Proof. intros. unfold Int.eq. rewrite Int.unsigned_not. @@ -3202,3 +3202,4 @@ Section CORRECTNESS. Qed. End CORRECTNESS. +*) |