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/RTLPargen.v | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

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

diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index e2e9a90..5ad3f90 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -473,9 +473,9 @@ Lemma sems_det:
   forall v v' mv mv',
   (sem_value A ge sp st f v /\ sem_value A tge sp st f v' -> v = v') /\
   (sem_mem A ge sp st f mv /\ sem_mem A tge sp st f mv' -> mv = mv').
-Proof. Admitted.
+Proof. Abort.
 
-Lemma sem_value_det:
+(*Lemma sem_value_det:
   forall A ge tge sp st f v v',
   ge_preserved ge tge ->
   sem_value A ge sp st f v ->
@@ -657,7 +657,7 @@ Lemma abstract_execution_correct:
     RTLBlock.step_instr_list ge sp (InstrState rs m) bb (InstrState rs' m') ->
     exists rs'', RTLPar.step_instr_block tge sp (InstrState rs m) bb' (InstrState rs'' m')
                  /\ regs_lessdef rs' rs''.
-Proof. Admitted.
+Proof. Abort.
 
 (*|
 Top-level functions
@@ -689,3 +689,4 @@ Definition transl_fundef := transf_partial_fundef transl_function_temp.
 
 Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program :=
   transform_partial_program transl_fundef p.
+*)
-- 
cgit