From 178a7c4781c96857fe0a33c777da83e769516152 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 11 Jul 2021 15:59:21 +0200
Subject: Remove unnecessary files and proofs

---
 src/hls/RTLPargenproof.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src/hls/RTLPargenproof.v')

diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index eb7931e..a0c01fa 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -16,7 +16,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-Require Import compcert.backend.Registers.
+(*Require Import compcert.backend.Registers.
 Require Import compcert.common.AST.
 Require Import compcert.common.Errors.
 Require Import compcert.common.Linking.
@@ -286,3 +286,4 @@ Section CORRECTNESS.
   Qed.*)
 
 End CORRECTNESS.
+*)
-- 
cgit