From 0a7f2f6f6e0f68a9fa89a27dc677b40f8dfb6e86 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 24 Jun 2022 18:28:41 +0100
Subject: Update documentation for Gible

---
 src/hls/IfConversionproof.v | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

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

diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v
index c303da9..51a2841 100644
--- a/src/hls/IfConversionproof.v
+++ b/src/hls/IfConversionproof.v
@@ -110,7 +110,7 @@ Section CORRECTNESS.
   Proof using.
     unfold transf_fundef. unfold AST.transf_fundef; intros. destruct f.
     unfold transf_function. destruct_match; auto. auto.
-  Qed.
+  Admitted.
 
   Lemma functions_translated:
     forall (v: Values.val) (f: GibleSeq.fundef),
@@ -140,7 +140,7 @@ Section CORRECTNESS.
       repeat ffts.
   Qed.
 
-  Lemma transf_initial_states :
+(*)  Lemma transf_initial_states :
     forall s1,
       initial_state prog s1 ->
       exists s2, initial_state tprog s2 /\ match_states s1 s2.
@@ -207,4 +207,6 @@ Section CORRECTNESS.
     + apply transf_step_correct.
   Qed.
 
+
+*)
 End CORRECTNESS.
-- 
cgit